Formal verification

<h2 id="approaches">Approaches</h2>
<h3>Model checking</h3>
<a href="/facts/Model_checking/FwvKMlw9">Model checking</a> involves a systematic and exhaustive exploration of the mathematical model. Such exploration is possible for <a href="/facts/Finite_model_theory/RkkjQbXp">finite models</a>, but also for some infinite models, where infinite sets of states can be effectively represented finitely by using abstraction or taking advantage of symmetry. Usually, this consists of exploring all states and transitions in the model, by using smart and domain-specific abstraction techniques to consider whole groups of states in a single operation and reduce computing time. Implementation techniques include <a href="/facts/State_space_enumeration/uHdJqm1w">state space enumeration</a>, symbolic state space enumeration, <a href="/facts/Abstract_interpretation/cj6wjzu1">abstract interpretation</a>, <a href="/facts/Symbolic_simulation/xmMhJP4N">symbolic simulation</a>, abstraction refinement. The properties to be verified are often described in <a href="/facts/Temporal_logic/vANP39lc">temporal logics</a>, such as <a href="/facts/Linear_temporal_logic/Gh5yxXK7">linear temporal logic</a> (LTL), <a href="/facts/Property_Specification_Language/2cGX8xlm">Property Specification Language</a> (PSL), <a href="/facts/SystemVerilog/wkBdc179">SystemVerilog</a> Assertions (SVA),<a class="footnote-ref" id="fnref:5" href="#fn:5">5</a> or <a href="/facts/Computational_tree_logic/h04gVzsL">computational tree logic</a> (CTL). The great advantage of model checking is that it is often fully automatic; its primary disadvantage is that it does not in general scale to large systems; symbolic models are typically limited to a few hundred bits of state, while explicit state enumeration requires the state space being explored to be relatively small.

<h3>Deductive verification</h3>
Another approach is deductive verification.<a class="footnote-ref" id="fnref:6" href="#fn:6">6</a><a class="footnote-ref" id="fnref:7" href="#fn:7">7</a> It consists of generating from the system and its specifications (and possibly other annotations) a collection of mathematical proof obligations, the truth of which imply conformance of the system to its specification, and discharging these obligations using either <a href="/facts/Proof_assistant/hjFGxLPn">proof assistants</a> (interactive theorem provers) (such as <a href="/facts/HOL_theorem_prover/xLdcpPeL">HOL</a>, <a href="/facts/ACL2/h1RX6FSe">ACL2</a>, <a href="/facts/Isabelle_(theorem_prover)/CNbtbX83">Isabelle</a>, <a href="/facts/Rocq_(software)/7oBXgLCE">Rocq</a> (previously known as Coq) or <a href="/facts/Prototype_Verification_System/WmEUheXc">PVS</a>), or <a href="/facts/Automated_theorem_proving/vKGvuKFI">automatic theorem provers</a>, including in particular <a href="/facts/Satisfiability_modulo_theories/10mBFLFB">satisfiability modulo theories</a> (SMT) solvers. This approach has the disadvantage that it may require the user to understand in detail why the system works correctly, and to convey this information to the verification system, either in the form of a sequence of theorems to be proved or in the form of specifications (invariants, preconditions, postconditions) of system components (e.g. functions or procedures) and perhaps subcomponents (such as loops or data structures).

<h3>Application to software</h3>
Formal verification of software programs involves proving that a program satisfies a formal specification of its behavior. Subareas of formal verification include deductive verification (see above), <a href="/facts/Abstract_interpretation/cj6wjzu1">abstract interpretation</a>, <a href="/facts/Automated_theorem_proving/vKGvuKFI">automated theorem proving</a>, <a href="/facts/Type_system/Tz0bAMS9">type systems</a>, and <a href="/facts/Formal_methods/tw4FCWIb">lightweight formal methods</a>. A promising type-based verification approach is <a href="/facts/Dependent_types/wCeQI7ds">dependently typed programming</a>, in which the types of functions include (at least part of) those functions' specifications, and type-checking the code establishes its correctness against those specifications. Fully featured dependently typed languages support deductive verification as a special case.
Another complementary approach is <a href="/facts/Program_derivation/uHEdeCxK">program derivation</a>, in which efficient code is produced from <a href="/facts/Functional_programming/cdxqPEIM">functional</a> specifications by a series of correctness-preserving steps. An example of this approach is the <a href="/facts/Bird%25E2%2580%2593Meertens_formalism/Us3fvK6D">Bird–Meertens formalism</a>, and this approach can be seen as another form of <a href="/facts/Program_synthesis/IK3gcrfp">program synthesis</a>.
These techniques can be <a href="/facts/Soundness/ndpamd2A">sound</a>, meaning that the verified properties can be logically deduced from the semantics, or unsound, meaning that there is no such guarantee. A sound technique yields a result only once it has covered the entire space of possibilities. An example of an unsound technique is one that covers only a subset of the possibilities, for instance only integers up to a certain number, and give a "good-enough" result. Techniques can also be <a href="/facts/Decidability_(logic)/17SHPMo0">decidable</a>, meaning that their algorithmic implementations are <a href="/facts/Termination_analysis/T740cWY7">guaranteed to terminate</a> with an answer, or undecidable, meaning that they may never terminate. By bounding the scope of possibilities, unsound techniques that are decidable might be able to be constructed when no decidable sound techniques are available.

<h2 id="verification-and-validation">Verification and validation</h2>
Main article: <a href="/facts/Verification_and_validation/hgqysrzb">Verification and validation</a>
Verification is one aspect of testing a product's fitness for purpose. Validation is the complementary aspect. Often one refers to the overall checking process as V & V.

<ul><li>Validation: "Are we trying to make the right thing?", i.e., is the product specified to the user's actual needs?</li>
<li>Verification: "Have we made what we were trying to make?", i.e., does the product conform to the specifications?</li></ul>
The verification process consists of static/structural and dynamic/behavioral aspects. E.g., for a software product one can inspect the source code (static) and run against specific test cases (dynamic). Validation usually can be done only dynamically, i.e., the product is tested by putting it through typical and atypical usages ("Does it satisfactorily meet all <a href="/facts/Use_case/8pNHjsIr">use cases</a>?").

<h2 id="automated-program-repair">Automated program repair</h2>
Main article: <a href="/facts/Automatic_bug_fixing/VoGYgrGf">Automatic bug fixing</a>
Program repair is performed with respect to an <a href="/facts/Oracle_(computability)/6ScMuvvY">oracle</a>, encompassing the desired functionality of the program which is used for validation of the generated fix. A simple example is a test-suite—the input/output pairs specify the functionality of the program. A variety of techniques are employed, most notably using <a href="/facts/Satisfiability_modulo_theories/10mBFLFB">satisfiability modulo theories</a> (SMT) solvers, and <a href="/facts/Genetic_programming/kGa2jr0w">genetic programming</a>,<a class="footnote-ref" id="fnref:8" href="#fn:8">8</a> using evolutionary computing to generate and evaluate possible candidates for fixes. The former method is deterministic, while the latter is randomized.
Program repair combines techniques from formal verification and <a href="/facts/Program_synthesis/IK3gcrfp">program synthesis</a>. Fault-localization techniques in formal verification are used to compute program points which might be possible bug-locations, which can be targeted by the synthesis modules. Repair systems often focus on a small pre-defined class of bugs in order to reduce the search space. Industrial use is limited owing to the computational cost of existing techniques.

<h2 id="industry-use">Industry use</h2>

The growth in complexity of designs increases the importance of formal verification techniques in the <a href="/facts/Electronics_industry/YX8VCvKC">hardware industry</a>.<a class="footnote-ref" id="fnref:9" href="#fn:9">9</a><a class="footnote-ref" id="fnref:10" href="#fn:10">10</a> At present, formal verification is used by most or all leading hardware companies,<a class="footnote-ref" id="fnref:11" href="#fn:11">11</a> but its use in the <a href="/facts/Software_industry/CJ81bC5P">software industry</a> is still languishing. This could be attributed to the greater need in the hardware industry, where errors have greater commercial significance. Because of the potential subtle interactions between components, it is increasingly difficult to exercise a realistic set of possibilities by simulation. Important aspects of hardware design are amenable to automated proof methods, making formal verification easier to introduce and more productive.<a class="footnote-ref" id="fnref:12" href="#fn:12">12</a>
As of 2011, several operating systems have been formally verified:
NICTA's Secure <a href="/facts/L4_microkernel_family/1rrWcHKB">Embedded L4 microkernel</a>, sold commercially as <a href="/facts/SeL4/1rrWcHKB">seL4</a> by OK Labs;<a class="footnote-ref" id="fnref:13" href="#fn:13">13</a> OSEK/VDX based real-time operating system ORIENTAIS by <a href="/facts/East_China_Normal_University/HXjlg9NB">East China Normal University</a>; Green Hills Software's <a href="/facts/Integrity_(operating_system)/9Dz1gPK2">Integrity operating system</a>; and <a href="/facts/SYSGO/uLX5Il0m">SYSGO</a>'s <a href="/facts/PikeOS/4uHGBKLf">PikeOS</a>.<a class="footnote-ref" id="fnref:14" href="#fn:14">14</a><a class="footnote-ref" id="fnref:15" href="#fn:15">15</a>
In 2016, a team led by Zhong Shao at Yale developed a formally verified operating system kernel called CertiKOS.<a class="footnote-ref" id="fnref:16" href="#fn:16">16</a><a class="footnote-ref" id="fnref:17" href="#fn:17">17</a>
As of 2017, formal verification has been applied to the design of large computer networks through a mathematical model of the network,<a class="footnote-ref" id="fnref:18" href="#fn:18">18</a> and as part of a new network technology category, <a href="/facts/Intent-Based_Networking/JMtYTvyv">intent-based networking</a>.<a class="footnote-ref" id="fnref:19" href="#fn:19">19</a> Network software vendors that offer formal verification solutions include <a href="/facts/Cisco/ocDgQt6T">Cisco</a><a class="footnote-ref" id="fnref:20" href="#fn:20">20</a> Forward Networks<a class="footnote-ref" id="fnref:21" href="#fn:21">21</a><a class="footnote-ref" id="fnref:22" href="#fn:22">22</a> and Veriflow Systems.<a class="footnote-ref" id="fnref:23" href="#fn:23">23</a>
The <a href="/facts/SPARK_(programming_language)/rQB6QTvf">SPARK programming language</a> provides a toolset which enables software development with formal verification and is <a href="/facts/SPARK_(programming_language)/rQB6QTvf">used in several high-integrity systems</a>.
The <a href="/facts/CompCert/pTVYRnuw">CompCert C compiler</a> is a formally verified C compiler implementing the majority of ISO C.<a class="footnote-ref" id="fnref:24" href="#fn:24">24</a><a class="footnote-ref" id="fnref:25" href="#fn:25">25</a>

<h2 id="see-also">See also</h2>

Look up verifiability in Wiktionary, the free dictionary.

<ul><li><a href="/facts/Automated_theorem_proving/vKGvuKFI">Automated theorem proving</a></li>
<li><a href="/facts/Model_checking/FwvKMlw9">Model checking</a></li>
<li><a href="/facts/List_of_model_checking_tools/N3aJ9UQ5">List of model checking tools</a></li>
<li><a href="/facts/Formal_equivalence_checking/WXHfJWGQ">Formal equivalence checking</a></li>
<li><a href="/facts/Proof_checker/hjFGxLPn">Proof checker</a></li>
<li><a href="/facts/Property_Specification_Language/2cGX8xlm">Property Specification Language</a></li>
<li><a href="/facts/Static_code_analysis/b56nr6QM">Static code analysis</a></li>
<li><a href="/facts/Temporal_logic_in_finite-state_verification/FwvKMlw9">Temporal logic in finite-state verification</a></li>
<li><a href="/facts/Post-silicon_validation/8otXdtpb">Post-silicon validation</a></li>
<li><a href="/facts/Intelligent_verification/j5AnMW8k">Intelligent verification</a></li>
<li><a href="/facts/Runtime_verification/pRHEYoDz">Runtime verification</a></li>
<li><a href="/facts/Software_verification/PczD7lsh">Software verification</a></li>
<li><a href="/facts/Hardware_verification/o4la3fmX">Hardware verification</a></li></ul>

<h2 id="references">References</h2>

<ol>
<li id="fn:1">Sanghavi, Alok (May 21, 2010). "What is formal verification?". EE Times Asia. <a href="#fnref:1" class="footnote-back-ref">↩</a></li>
<li id="fn:2">"Common Criteria for Information Technology Security Evaluation Part 5: Pre-defined packages of security requirements" (PDF). Retrieved April 15, 2025. <a href="https://www.commoncriteriaportal.org/files/ccfiles/CC2022PART5R1.pdf" target="_blank">https://www.commoncriteriaportal.org/files/ccfiles/CC2022PART5R1.pdf</a> <a href="#fnref:2" class="footnote-back-ref">↩</a></li>
<li id="fn:3">Sanjit A. Seshia; Natasha Sharygina; Stavros Tripakis (2018). "Chapter 3: Modeling for Verification". In Clarke, Edmund M.; Henzinger, Thomas A.; Veith, Helmut; Bloem, Roderick (eds.). Handbook of Model Checking. Springer. pp. 75–105. doi:10.1007/978-3-319-10575-8. ISBN 978-3-319-10574-1. <a href="978-3-319-10574-1" target="_blank">978-3-319-10574-1</a> <a href="#fnref:3" class="footnote-back-ref">↩</a></li>
<li id="fn:4">Introduction to Formal Verification, Berkeley University of California, Retrieved November 6, 2013 <a href="http://embedded.eecs.berkeley.edu/research/vis/doc/VisUser/vis_user/node4.html" target="_blank">http://embedded.eecs.berkeley.edu/research/vis/doc/VisUser/vis_user/node4.html</a> <a href="#fnref:4" class="footnote-back-ref">↩</a></li>
<li id="fn:5">Cohen, Ben; Venkataramanan, Srinivasan; Kumari, Ajeetha; Piper, Lisa (2015). SystemVerilog Assertions Handbook (4th ed.). CreateSpace Independent Publishing Platform. ISBN 978-1518681448. <a href="978-1518681448" target="_blank">978-1518681448</a> <a href="#fnref:5" class="footnote-back-ref">↩</a></li>
<li id="fn:6">Ahrendt, Wolgang; Beckert, Bernhard; Bubel, Richard; Hähnle, Reiner; Schmitt, Peter H., eds. (2016). Deductive Software Verification - The KeY Book: From Theory to Practice (1st 2016 ed.). Cham: Springer International Publishing : Imprint: Springer. ISBN 978-3-319-49812-6. <a href="978-3-319-49812-6" target="_blank">978-3-319-49812-6</a> <a href="#fnref:6" class="footnote-back-ref">↩</a></li>
<li id="fn:7">Pretschner, Alexander; Müller, Peter; Stöckle, Patrick, eds. (2019). "Building Deductive Program Verifiers - Lecture Notes". Engineering secure and dependable software systems. Amsterdam, Netherlands: IOS Press. ISBN 978-1-61499-976-8. <a href="978-1-61499-976-8" target="_blank">978-1-61499-976-8</a> <a href="#fnref:7" class="footnote-back-ref">↩</a></li>
<li id="fn:8">Le Goues, Claire; Nguyen, ThanhVu; Forrest, Stephanie; Weimer, Westley (January 2012). "GenProg: A Generic Method for Automatic Software Repair". IEEE Transactions on Software Engineering. 38 (1): 54–72. doi:10.1109/TSE.2011.104. S2CID 4111307. <a href="/wiki/Claire_Le_Goues" target="_blank">/wiki/Claire_Le_Goues</a> <a href="#fnref:8" class="footnote-back-ref">↩</a></li>
<li id="fn:9">Harrison, J. (2003). "Formal verification at Intel". 18th Annual IEEE Symposium of Logic in Computer Science, 2003. Proceedings. pp. 45–54. doi:10.1109/LICS.2003.1210044. ISBN 978-0-7695-1884-8. S2CID 44585546. <a href="978-0-7695-1884-8" target="_blank">978-0-7695-1884-8</a> <a href="#fnref:9" class="footnote-back-ref">↩</a></li>
<li id="fn:10">Formal verification of a real-time hardware design. Portal.acm.org (June 27, 1983). Retrieved on April 30, 2011. <a href="http://portal.acm.org/citation.cfm?id=800667" target="_blank">http://portal.acm.org/citation.cfm?id=800667</a> <a href="#fnref:10" class="footnote-back-ref">↩</a></li>
<li id="fn:11">"Formal Verification: An Essential Tool for Modern VLSI Design by Erik Seligman, Tom Schubert, and M V Achutha Kirankumar". 2015. <a href="http://formalverificationbook.com" target="_blank">http://formalverificationbook.com</a> <a href="#fnref:11" class="footnote-back-ref">↩</a></li>
<li id="fn:12">"Formal Verification in Industry" (PDF). Retrieved September 20, 2012. <a href="http://www.cl.cam.ac.uk/~jrh13/slides/types-04sep99/slides1.pdf" target="_blank">http://www.cl.cam.ac.uk/~jrh13/slides/types-04sep99/slides1.pdf</a> <a href="#fnref:12" class="footnote-back-ref">↩</a></li>
<li id="fn:13">"Abstract Formal Specification of the seL4/ARMv6 API" (PDF). Archived from the original (PDF) on May 21, 2015. Retrieved May 19, 2015. <a href="https://web.archive.org/web/20150521171234/https://sel4.systems/Docs/seL4-spec.pdf" target="_blank">https://web.archive.org/web/20150521171234/https://sel4.systems/Docs/seL4-spec.pdf</a> <a href="#fnref:13" class="footnote-back-ref">↩</a></li>
<li id="fn:14">Christoph Baumann, Bernhard Beckert, Holger Blasum, and Thorsten Bormer Ingredients of Operating System Correctness? Lessons Learned in the Formal Verification of PikeOS Archived July 19, 2011, at the Wayback Machine <a href="http://www-wjp.cs.uni-saarland.de/publikationen/Ba10EW.pdf" target="_blank">http://www-wjp.cs.uni-saarland.de/publikationen/Ba10EW.pdf</a> <a href="#fnref:14" class="footnote-back-ref">↩</a></li>
<li id="fn:15">"Getting it Right" by Jack Ganssle <a href="http://www.ganssle.com/rants/gettingitright.htm" target="_blank">http://www.ganssle.com/rants/gettingitright.htm</a> <a href="#fnref:15" class="footnote-back-ref">↩</a></li>
<li id="fn:16">Harris, Robin. "Unhackable OS? CertiKOS enables creation of secure system kernels". ZDNet. Retrieved June 10, 2019. <a href="https://www.zdnet.com/article/certikos-a-hacker-proof-os/" target="_blank">https://www.zdnet.com/article/certikos-a-hacker-proof-os/</a> <a href="#fnref:16" class="footnote-back-ref">↩</a></li>
<li id="fn:17">"CertiKOS: Yale develops world's first hacker-resistant operating system". International Business Times UK. November 15, 2016. Retrieved June 10, 2019. <a href="https://www.ibtimes.co.uk/certikos-yale-develops-worlds-first-hacker-resistant-operating-system-1591712" target="_blank">https://www.ibtimes.co.uk/certikos-yale-develops-worlds-first-hacker-resistant-operating-system-1591712</a> <a href="#fnref:17" class="footnote-back-ref">↩</a></li>
<li id="fn:18">Scroxton, Alex. "For Cisco, intent-based networking heralds future tech demands". Computer Weekly. Retrieved February 12, 2018. <a href="http://www.computerweekly.com/news/252434028/For-Cisco-intent-based-networking-heralds-future-tech-demands" target="_blank">http://www.computerweekly.com/news/252434028/For-Cisco-intent-based-networking-heralds-future-tech-demands</a> <a href="#fnref:18" class="footnote-back-ref">↩</a></li>
<li id="fn:19">Lerner, Andrew. "Intent-based networking". Gartner. Retrieved February 12, 2018. <a href="https://blogs.gartner.com/andrew-lerner/2017/02/07/intent-based-networking/" target="_blank">https://blogs.gartner.com/andrew-lerner/2017/02/07/intent-based-networking/</a> <a href="#fnref:19" class="footnote-back-ref">↩</a></li>
<li id="fn:20">Kerravala, Zeus. "Cisco brings intent based networks to the data center". NetworkWorld. Archived from the original on December 11, 2023. Retrieved February 12, 2018. <a href="https://www.networkworld.com/article/965142/cisco-brings-intent-based-networks-to-the-data-center.html" target="_blank">https://www.networkworld.com/article/965142/cisco-brings-intent-based-networks-to-the-data-center.html</a> <a href="#fnref:20" class="footnote-back-ref">↩</a></li>
<li id="fn:21">"Forward Networks: Accelerating and De-risking Network Operations". Insightssuccess Media and Technology Pvt. Ltd. Insights Success. January 16, 2018. Retrieved February 12, 2018. <a href="http://www.insightssuccess.com/forward-networks-accelerating-de-risking-network-operations/" target="_blank">http://www.insightssuccess.com/forward-networks-accelerating-de-risking-network-operations/</a> <a href="#fnref:21" class="footnote-back-ref">↩</a></li>
<li id="fn:22">"Getting Grounded in Intent=based Networking" (PDF). NetworkWorld. Retrieved February 12, 2018. <a href="https://images.idgesg.net/assets/2018/01/idg_2018_intent-based_networking.pdf" target="_blank">https://images.idgesg.net/assets/2018/01/idg_2018_intent-based_networking.pdf</a> <a href="#fnref:22" class="footnote-back-ref">↩</a></li>
<li id="fn:23">"Veriflow Systems". Bloomberg. Retrieved February 12, 2018. <a href="https://www.bloomberg.com/research/stocks/private/snapshot.asp?privcapid=274750862" target="_blank">https://www.bloomberg.com/research/stocks/private/snapshot.asp?privcapid=274750862</a> <a href="#fnref:23" class="footnote-back-ref">↩</a></li>
<li id="fn:24">"CompCert - The CompCert C compiler". compcert.org. Retrieved February 22, 2023. <a href="https://compcert.org/compcert-C.html" target="_blank">https://compcert.org/compcert-C.html</a> <a href="#fnref:24" class="footnote-back-ref">↩</a></li>
<li id="fn:25">Barrière, Aurèle; Blazy, Sandrine; Pichardie, David (January 9, 2023). "Formally Verified Native Code Generation in an Effectful JIT: Turning the CompCert Backend into a Formally Verified JIT Compiler". Proceedings of the ACM on Programming Languages. 7 (POPL): 249–277. arXiv:2212.03129. doi:10.1145/3571202. ISSN 2475-1421. S2CID 253736486. <a href="/wiki/Sandrine_Blazy" target="_blank">/wiki/Sandrine_Blazy</a> <a href="#fnref:25" class="footnote-back-ref">↩</a></li>
</ol>

Formal verification open-in-new

Formal verification