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 vulnerabilities which are hard to detect manually or by 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 is a leading example of a formal verification tool for smart contracts. We note that formal specifications have benefits beyond formal verification — they are good conceptual tools and also make testing and fuzzing more automatic."
