Tools to build cryptographic software that is correct and secure by construction
We're building tools to generate cryptographic implementations with machine-checked mathematical proofs of correctness and security, via the Coq proof assistant.
Our first project was Fiat Cryptography, a domain-specific, formally verified compiler for cryptographic arithmetic. Today it drives important parts of (elliptic-curve-based) TLS in both Chrome and Firefox, and it has been adopted by a few other open-source projects.
We are now studying a number of higher- and lower-level extensions, including security proofs of protocols, proof-generating compilation of protocol descriptions to executable code, correct-by-construction generation of code for parts of crypto libraries beyond just finite-field arithmetic, and generation of proved assembly code rather than just C.
