sorryfreeLast reviewed 2026-09-13
Index › Frameworks › Certora Prover

Certora Prover

Direct answerCertora Prover verifies smart contracts against rules written in CVL, on EVM, Solana, Move and Soroban. It is the tool to verify the on-chain verifier and bridge logic around a ZK system; it does not verify circuits.
Maintainer
Certora
Website
https://github.com/Certora/CertoraProver
Repository
https://github.com/Certora/CertoraProver
Category
Proof assistants and general verifiers
Targets
SolidityVyperSolana (Rust)MoveSoroban
Approach
Rule-based specification (CVL) discharged by SMT over bytecode
Access
Open source (2025)
Status (2026-09-13)
Active

Last reviewed 2026-09-13 by the sorryfree editors.

What Certora Prover does

Open-sourced in 2025, it is the most used contract-level prover. Halmos and hevm are lighter symbolic alternatives.

Where it is strong

  • Production usage across DeFi.
  • Multi-chain.
  • Open source with commercial support.

Limits and caveats

  • Not cryptography-specific.
  • SMT timeouts on complex invariants.
  • Rules must be written and reviewed.

When to choose it

Use it for the verifier contract, bridge and upgrade logic of a ZK deployment.

Who works with Certora Prover

Certora.

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

Lean 4 and Mathlib, Rocq (formerly Coq), Isabelle/HOL, F*, ACL2 (R1CS and PFCS books), K framework and KEVM.

Sources

Last reviewed 2026-09-13 by the sorryfree editors. Machine-readable: data.json · summary.txt