Formal Verification

From CryptoWiki

Revision as of 01:42, 13 October 2022 by Grand Master Pepe (talk | contribs) (Created page with "From Secureum (2-10-2022): 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 tra...")
(diff) ← Older revision | Latest revision (diff) | Newer revision → (diff)

From Secureum (2-10-2022): 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.

Retrieved from "https://cryptowiki.me/index.php?title=Formal_Verification&oldid=17177"