EasyCrypt: Computational security proofs with relational Hoare logic
====================================================================

EasyCrypt 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: Active, mature
Strengths: 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: Steep learning curve; small pool of practitioners. | Proofs do not transfer automatically to code outside Jasmin. | Not a circuit tool.
Firms using it: Nethermind (Formal Verification team)
Sources: https://easycrypt.info | https://formosa-crypto.org

Source page: https://sorryfree.com/frameworks/easycrypt/
Compiled by: sorryfree editors (https://sorryfree.com/about/)
Last reviewed: 2026-09-13