Smart-contract formal verification
Prove your contracts behave as specified.
CertiK Prover checks precise specifications against your Solidity code, reasoning across every allowed input and starting state in a confirmed scope — evidence example-based tests cannot give on their own.
What a verification involves
01
Code
The Solidity implementation that runs on chain.
02
Specification
The behavior claimed for the selected code, written so it can be checked.
03
Result
What CertiK Prover established for that claim, with its scope stated.
User guide
Start with the user guide
Install CertiK Prover, write and check your first specification, then learn everything specifications can express.