Difference between revisions of "Formal Verification"
(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...") |
m |
||
| Line 1: | Line 1: | ||
From [[Secureum]] (2-10-2022): | * [https://secureum.substack.com/p/aave-certora-secureum-collaboration From] [[Secureum]] (2-10-2022): | ||
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 | ''"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|Certora’s]] Prover is a leading example of a formal verification tool for [[Smart Contract (SC)|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."'' | |||
[[Category:Jargon/Various]] | |||
Latest revision as of 01:48, 13 October 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."
