Rocq (formerly Coq)
Direct answerRocq, the renamed Coq, underpins Fiat-Crypto's verified field arithmetic, SSProve's computational proofs, Formal Land's Garden circuit framework and its rocq-of-rust and rocq-of-solidity translators. It is the main alternative to Lean for cryptographic verification.
- Maintainer
- Inria and the Rocq community
- Website
- https://rocq-prover.org
- Category
- Proof assistants and general verifiers
- Targets
- Fiat-CryptoSSProveGardenrocq-of-rustrocq-of-solidity
- Approach
- Interactive theorem prover based on the calculus of inductive constructions
- Access
- Open source (LGPL)
- Status (2026-09-13)
- Active
What Rocq (formerly Coq) does
Rocq's strength in cryptography is its implementation-verification lineage. CertiCrypt, the ancestor of EasyCrypt, was built on it.
Where it is strong
- Mature, stable, well documented.
- Strong extraction to executable code.
- Formal Land's Rust and Solidity translators.
Limits and caveats
- ZK ecosystem momentum is with Lean.
- Steeper syntax for newcomers.
- Fewer circuit-specific libraries.
When to choose it
Choose Rocq when your team or partner is Rocq-native, or to reuse Fiat-Crypto and rocq-of-rust.
Who works with Rocq (formerly Coq)
Top-listed for proof engineering 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 assistants and general verifiers
Lean 4 and Mathlib, Isabelle/HOL, F*, ACL2 (R1CS and PFCS books), K framework and KEVM, Certora Prover.