hacspec
ConCert
| hacspec | ConCert | |
|---|---|---|
| 3 | 1 | |
| 235 | 108 | |
| - | 1.9% | |
| 5.1 | 8.0 | |
| 3 months ago | 3 months ago | |
| Coq | Coq | |
| MIT License | MIT License |
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
ConCert
-
Rustlang Cryptography Interest Group & Formal Verification Sync-up Call 2
Bas Spitter will be speaking on Hacspec and ConCert
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]
vericert - A formally verified high-level synthesis tool based on CompCert and written in Coq.
rust-crypto - A (mostly) pure-Rust implementation of various cryptographic algorithms.
scilla - Scilla - A Smart Contract Intermediate Level Language
proofs - My personal repository of formally verified mathematics.
Doubly-Linked-List-VST - The final project for CS2603 (2021 Spring), aiming to verify a doubly linked list library using VST. Collaborating with @karzexcc
zips - Zcash Improvement Proposals
toychain - A minimalistic blockchain consensus implemented and verified in Coq
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