Certora Prover: SMT-based verification of smart contracts, including ZK verifier contracts
================================================================================

Certora 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
Category: Proof assistants and general verifiers
Targets: Solidity, Vyper, Solana (Rust), Move, Soroban
Approach: Rule-based specification (CVL) discharged by SMT over bytecode
Access: Open source (2025)
Status: Active
Strengths: Production usage across DeFi. | Multi-chain. | Open source with commercial support.
Limits: Not cryptography-specific. | SMT timeouts on complex invariants. | Rules must be written and reviewed.
Firms using it: Certora
Sources: https://github.com/Certora/CertoraProver

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