26 - Formal Verification
Formal verification is the act of proving or disproving the correctness of intended algorithms underlying a system with respect to a certain formal specification or property, using formal methods of mathematics
- Formal verification is effective at detecting complex bugs which are hard to detect manually or using simpler automated tools
- Formal verification needs a specification of the program being verified and techniques to translate/compare the specification with the actual implementation
- Certora’s Prover and ChainSecurity’s VerX are examples of formal verification tools for smart contracts. KEVM from Runtime Verification Inc is a formal verification framework that models EVM semantics.
