Tool selection guide
Formal verification tools: specifications and proof boundaries
A proof answers a property under a model. Decide which property matters, which implementation is represented and which environmental behavior the model assumes. A proof of arithmetic behavior inside a function does not automatically cover oracle trust, account authorization or later upgrades.
Sources checked . Documentation interpretation; no solver run was performed.
Read about what a smart contract proof does and does not establish.
Decide what your review needs
- Name the property and the code revision before choosing a verifier. Make the expected behavior reviewable by someone who did not write the specification.
- List assumptions and abstractions explicitly, including external calls, summaries and valid initial states.
- Treat timeout, unsupported behavior and an unknown solver outcome separately from a proved property.
- Match the verifier to the implementation language and execution model. Rust checking does not supply Solana signer and account rules unless the harness models them.
Compare inputs, results and limits
| Tool & access | Input → output | When it fits | Limits & source |
|---|---|---|---|
| Certora Prover EVM | Input: Contract code with CVL rules and configuration Output: Rule-specific verification results and counterexamples | You can maintain a specification and review environmental summaries for the engagement. | Specifications, summaries and environmental assumptions define what a successful proof establishes. Documentation reviewed. Official source |
| Solidity SMTChecker EVM | Input: Solidity source with selected model-checker engines and assertions Output: Compiler-reported proof outcomes or potential violations | You need compiler-integrated checking of supported properties and can interpret engine limits. | Review unsupported features and solver results. An inconclusive result is not a proof. Documentation reviewed. Official source |
| Kani Rust | Input: Rust code and a proof harness Output: Bounded model-checking results or counterexamples | The target is Rust behavior that you can represent in a harness, with explicit bounds and assumptions. | Bounds and modeled Rust behavior limit coverage. Chain-specific account rules need separate properties. Documentation reviewed. Official source |
Public artifact walkthrough
Separate "happens" from "might happen" in SMTChecker output
Solidity's documentation separates a proved failure from a case the solver could not settle within its limits. It also explains that require conditions become assumptions and assert conditions define properties to prove. Review whether an assumption accidentally excludes the attack state before relying on a successful property. Record the engine and selected targets; enabling no engine produces no verification result.
- Write one property and list the states admitted by its assumptions. Include a hostile state unless the system actually prevents it.
- For each run, retain the engine, configuration and complete outcome. Classify unknown results separately.
- Have a reviewer challenge the specification against the intended protocol rule before accepting a proof as scoped evidence.