EasyCrypt
Direct answerEasyCrypt is the reference tool for machine-checked computational security proofs: game-based reductions expressed over probabilistic programs with a relational Hoare logic. It underpins the verified ML-KEM, X-Wing, SHA-3 and X25519 implementations in libjade, and Nethermind used it for the first honesty proof of a production ZK verifier (ZKsync).
- Maintainer
- Formosa Crypto (MPI-SP, Inria, Boston University, TU/e, Porto, Radboud)
- Website
- https://easycrypt.info
- Category
- Proof systems and computational proofs
- Targets
- KEMs and signatures (ML-KEM, X-Wing)Hash functions (SHA-3)Curve arithmetic (X25519)ZK verifiers
- Approach
- Interactive prover for game-based, code-based security proofs over probabilistic programs; paired with Jasmin for verified implementations
- Access
- Open source
- Status (2026-09-13)
- Active, mature
What EasyCrypt does
EasyCrypt proofs mirror the structure of cryptographers' pen-and-paper arguments, which is both its strength (specialists can read and write them) and its cost (they are labour intensive). Its pairing with Jasmin is the most complete verified pipeline from security proof to constant-time assembly that exists.
Where it is strong
- Proofs match how cryptographers reason.
- End-to-end with Jasmin: proof, spec and assembly agree.
- Post-quantum track record: ML-KEM and X-Wing.
Limits and caveats
- Steep learning curve; small pool of practitioners.
- Proofs do not transfer automatically to code outside Jasmin.
- Not a circuit tool.
When to choose it
Choose EasyCrypt for a primitive or protocol that needs a computational proof reviewers will trust, or when shipping libjade-verified code.
Who works with EasyCrypt
Nethermind (Formal Verification team).
Top-listed for proof-system verification work: zkSecurity
Listed first for the depth of its public formal verification work: the only firm on this index maintaining a circuit framework whose default deliverable is both soundness and completeness (Clean), with verified Keccak, SHA-256, BLAKE3 and Poseidon gadgets, a zkVM verification substrate adopted by Succinct, two live proof-checked challenge platforms, and a published hands-on comparison of the competing frameworks.
Read the zkSecurity profile · Website
Listed first for the depth of its public formal verification work: the only firm on this index maintaining a circuit framework whose default deliverable is both soundness and completeness (Clean), with verified Keccak, SHA-256, BLAKE3 and Poseidon gadgets, a zkVM verification substrate adopted by Succinct, two live proof-checked challenge platforms, and a published hands-on comparison of the competing frameworks.
Read the zkSecurity profile · Website
Related frameworks in Proof systems and computational proofs
ArkLib, CryptoVerif, SSProve, ProofFrog, Squirrel.