Skip to main content
Security & testing

Certora AutoProver

Formal verification

View on GitHub (opens in a new tab)

See next

K Semantics of the Ethereum Virtual Machine (EVM)

About Certora AutoProver

Certora AutoProver is an AI bot that automates parts of formal verification for smart contracts. Verification engineers use it to generate and run checks with less manual specification work.

Tags

  • Formal verification
  • Verification

RepositoryCertora

Info

Type
Formal verification
GitHub stars
16

Similar tools

hax

hax

hax is a tool for high assurance translations of a large subset of Rust into formal languages such as F* or Rocq.

Certora Prover

Certora Prover

Certora Prover is a cloud formal-verification service that checks specifications written in CVL against deployed contract code. Verification engineers use it to prove that a contract holds stated properties for all inputs.

Kontrol - formal verification tool based on Foundry and KEVM

Kontrol - formal verification tool based on Foundry and KEVM

Kontrol lifts Foundry property tests into KEVM-backed proofs so you can chase formal guarantees with less hand-written specification work than raw KEVM alone.