hacspec
hacspec
Stars - the number of stars that a project has on GitHub. Growth - month over month growth in stars.
Activity is a relative number indicating how actively a project is being developed. Recent commits have higher weight than older ones.
For example, an activity of 9.0 indicates that a project is amongst the top 10% of the most actively developed projects that we are tracking.
hacspec
-
Bertie – A minimal, high-assurance implementation of TLS 1.3 written in hacspec
I have no idea what the legal weight is for a toml field so this repo really would benefit from having a formal copy of the Apache-2 license file https://github.com/hacspec/hax/blob/2da100068e9ae5e69e5b35bb... similar to its MIT friend https://github.com/hacspec/hacspec/blob/4ecc847fc944fe996e19...
-
Lets goo memory safe asm
†The "Rust" code would most likely need to be written in a strict subset of the language like Hacspec
-
Rustlang Cryptography Interest Group & Formal Verification Sync-up Call 2
Bas Spitter will be speaking on Hacspec and ConCert
hacspec
-
Bertie – A minimal, high-assurance implementation of TLS 1.3 written in hacspec
hacspec
> This is the successor of https://github.com/HACS-workshop/hacspec but a predecessor of https://github.com/hacspec/hax. Development in this repository has mostly stopped, see hax instead.
What are some alternatives?
creusot - Creusot helps you prove your code is correct in an automated fashion. [Moved to: https://github.com/creusot-rs/creusot]
ConCert - A framework for smart contract verification in Coq
rust-crypto - A (mostly) pure-Rust implementation of various cryptographic algorithms.
proofs - My personal repository of formally verified mathematics.
zips - Zcash Improvement Proposals
silveroak - Formal specification and verification of hardware, especially for security and privacy.
magmide - A dependently-typed proof language intended to make provably correct bare metal code possible for working software engineers.
bertie - Bertie TLS 1.3 Implementation