Differences between Solidity SMTChecker and Certora prover

Is anyone familiar with SMTChecker introduced in solidity 0.8.10. How is it different from formal verification tools created by Certora?

While both SMTChecker and the Certora Prover have the goal of proving properties about your code, there are many differences both in how these properties are specified and the mechanisms used for verifying them.

The main differences are:

(1) We operate on the bytecode level while SMTChecker checks the Solidity code. This means the Certora Prover can discover bugs in the Solidity compiler.
(2) We allow for a rich specification language that can go beyond asserts in Solidity, e.g., checking contract-wide invariants, and relational properties.
(3) The Certora tool is developed by an entire team of formal verification experts working on scaling the verification to larger and more complicated code, including whole contract systems.
(4) Certora offers spec-checking tools, counterexample presentation, integrations with VScode and CI/CD, and other utilities to render the user experience smooth.

2 Likes