Rocq (formerly Coq): Proof assistant behind Fiat-Crypto, SSProve, Garden and rocq-of-rust
================================================================================

Rocq, 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-Crypto, SSProve, Garden, rocq-of-rust, rocq-of-solidity
Approach: Interactive theorem prover based on the calculus of inductive constructions
Access: Open source (LGPL)
Status: Active
Strengths: Mature, stable, well documented. | Strong extraction to executable code. | Formal Land's Rust and Solidity translators.
Limits: ZK ecosystem momentum is with Lean. | Steeper syntax for newcomers. | Fewer circuit-specific libraries.
Firms using it: Formal Land
Sources: https://rocq-prover.org

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