Related Projects
- miTLS (https://mitls.org) - a verified reference implementation of TLS
- HACL* (https://github.com/project-everest/hacl-star) - a verified library of cryptographic primitives
- Vale (https://github.com/project-everest/vale) - Verfied Assembly Language for Everest
- F* (https://fstar-lang.org) - a verification language for effectful programs; used by miTLS, HACL*, and Vale
- KreMLin (https://github.com/FStarLang/kremlin/) - a compiler from a subset of F* to C; used by miTLS and HACL*
- Z3 (https://github.com/Z3Prover/z3) - SMT solver; used by F* and Dafny
- Dafny (https://github.com/Microsoft/dafny) - a program verifier; used by Vale
- IronClad (https://github.com/Microsoft/Ironclad) - provably secure and reliable systems
- Lean (https://leanprover.github.io/) - Interactive theorem prover