Certora AutoProver public release

AutoProver for Solidity

AutoProver turns contract intent into formal properties and verifies generated CVL rules with the Certora Prover. A standalone run targets one Solidity contract, keeps the design document and threat model optional, and reports both verified behavior and gaps that need review.

AutoFuzzer and All in one

AutoFuzzer generates and executes Foundry tests for one Solidity contract. All in one combines AI Auditor findings, AutoProver formal verification, and AutoFuzzer test generation in a single dashboard run.

Reports and generated files

Reports separate findings, formal-verification outcomes, test-generation results, and generated artifacts. When eligible files are available, you can propose CVL specifications or Foundry tests back to the repository from the report.

See the AutoProver User Manual for setup, engine selection, billing, and troubleshooting.