Proof assistants and general verifiers used in cryptography: Lean 4, Rocq, Isabelle, F*, ACL2, K, Certora Prover
================================================================================

The foundations underneath the specialised frameworks: interactive proof assistants (Lean 4, Rocq, Isabelle/HOL, F*, ACL2), a semantics framework (K), and SMT-based verifiers for smart contracts (Certora Prover, Halmos, hevm). Choosing one fixes the ecosystem, the available libraries, the hiring pool and, increasingly, which AI proving tools can help.

Lean 4 and Mathlib: Lean FRO and the Mathlib community — Clean, zkLean, Halva, ArkLib, sp1-lean, Lampe, EvmYul, Cairo AIR proofs — Interactive theorem prover with a small trusted kernel, a large mathematics library and a growing AI-prover ecosystem — Active
Rocq (formerly Coq): Inria and the Rocq community — Fiat-Crypto, SSProve, Garden, rocq-of-rust, rocq-of-solidity — Interactive theorem prover based on the calculus of inductive constructions — Active
Isabelle/HOL: TU München and University of Cambridge — C and ARM64 via AutoCorres2, Apple corecrypto — Higher-order logic with strong automation; refinement via AutoCorres2 — Active
F*: Microsoft Research and Inria — HACL*, hax (main backend), DY*, libcrux — Dependently typed effectful programming with SMT automation; extraction to C and OCaml — Active
ACL2 (R1CS and PFCS books): ACL2 community (Kestrel Institute) — R1CS, Prime-field constraint systems, acl2-jolt — First-order logic with strong automation; R1CS and PFCS libraries; acl2-jolt for Jolt circuits — Mature, niche
K framework and KEVM: Runtime Verification — EVM (KEVM), zkevm-harness, Lean backend for K — Rewriting-based semantics from which interpreters, symbolic executors and provers are derived — Active, mature
Certora Prover: Certora — Solidity, Vyper, Solana (Rust), Move, Soroban — Rule-based specification (CVL) discharged by SMT over bytecode — Active
How to choose: New ZK verification project in 2026: **Lean 4**. The libraries, the funded projects and the AI provers are there. | Rust implementation verification with a Rocq team, or reuse of Fiat-Crypto: **Rocq**. | C and ARM64 code with a refinement-style methodology: **Isabelle/HOL** with AutoCorres2, as Apple did. | Executable semantics that both runs and proves (EVM, zkVM ISAs): the **K framework**. | On-chain verifier contract properties: **Certora Prover** for full rule-based verification, **Halmos** or **hevm** for bounded symbolic checks.

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