← All repos

easycrypt

EasyCrypt: Computer-Aided Cryptographic Proofs

GitHub
Browse cluster: Lean4 Formal Verification & Cryptography →
6,178commits
78contributors
13languages

Tech stack & purpose

EasyCrypt is a proof assistant and toolset for reasoning about the security of cryptographic constructions through computer-aided formal verification. It supports probabilistic computations, multiple program logics including Hoare logic and probabilistic relational Hoare logic, and is designed to handle code-based cryptographic security proofs as well as functional correctness verification of low-level implementations, particularly those written in Jasmin. The tool is built in OCaml and integrates with Why3 (version >= 1.8 and < 1.9) and SMT solvers such as Alt-Ergo, CVC5, and Z3 to discharge proof obligations. EasyCrypt is part of the Formosa Crypto project and provides interactive development through Proof General (Emacs) and has a Visual Studio Code front-end in development.

Community & reference links

Languages

OCaml
67.3%
eC
30.7%
Python
0.9%
Shell
0.5%
TeX
0.1%
Dockerfile
0.1%
C
0.1%
CSS
0.1%
Makefile
0.1%
Nix
0.1%
Dune
0.0%
Emacs Lisp
0.0%
Batchfile
0.0%

Contributors (top 30 of 78)