Editing Formal verification (section)

{{short description|Proving or disproving the correctness of certain intended algorithms}}
{{hatnote group|
{{Distinguish|Verificationism}}
{{for|the Wikipedia policy|Wikipedia:Verifiability|selfref=true}}
}}
{{Use mdy dates|date=June 2019}}

In the context of [[Computer hardware|hardware]] and [[software]] systems, '''formal verification''' is the act of [[Mathematical proof|proving]] or disproving the [[correctness (computer science)|correctness]] of a system with respect to a certain [[formal specification]] or property, using [[formal methods]] of [[mathematics]].<ref>{{cite journal|last=Sanghavi|first=Alok|title=What is formal verification?|journal=EE Times Asia|date=May 21, 2010}}</ref> 
Formal verification is a key incentive for [[formal specification]] of systems, and is at the core of [[formal methods]].
It represents an important dimension of [[Electronic design automation#Analysis and verification|analysis and verification]] in [[electronic design automation]] and is one approach to [[software verification]]. The use of formal verification enables the highest [[Evaluation Assurance Level]] ([[EAL7]]) in the framework of [[common criteria]] for [[computer security]] certification.<ref>{{cite web |url=https://www.commoncriteriaportal.org/files/ccfiles/CC2022PART5R1.pdf |title=Common Criteria for Information Technology Security Evaluation Part 5: Pre-defined packages of security requirements |access-date=April 15, 2025}}</ref>

Formal verification can be helpful in proving the correctness of systems such as: [[cryptographic protocol]]s, [[Combinational logic|combinational circuits]], [[digital circuit]]s with internal memory, and software expressed as [[source code]] in a [[programming language]]. Prominent examples of verified software systems include the [[CompCert]] verified [[C programming language|C]] [[compiler]] and the [[L4 microkernel family#High assurance: seL4|seL4]] high-assurance [[Kernel (operating system)|operating system kernel]].

The verification of these systems is done by ensuring the existence of a [[formal proof]] of a [[mathematical model]] of the system.<ref>{{cite book |editor1=Clarke, Edmund M. |editor2=Henzinger, Thomas A. |editor3=Veith, Helmut |editor4=Bloem, Roderick |author1=Sanjit A. Seshia |author2=Natasha Sharygina |author3=Stavros Tripakis |title=Handbook of Model Checking |date=2018 |publisher=Springer |isbn=978-3-319-10574-1 |pages=75–105 |url=https://doi.org/10.1007/978-3-319-10575-8 |chapter=Chapter 3: Modeling for Verification|doi=10.1007/978-3-319-10575-8 }}</ref> Examples of mathematical objects used to model systems are: [[finite-state machine]]s, [[labelled transition system]]s, [[Horn clause]]s, [[Petri net]]s, [[vector addition system]]s, [[timed automaton|timed automata]], [[hybrid automata]], [[process algebra]], formal semantics of programming languages such as [[operational semantics]], [[denotational semantics]], [[axiomatic semantics]] and [[Hoare logic]].<ref>[http://embedded.eecs.berkeley.edu/research/vis/doc/VisUser/vis_user/node4.html Introduction to Formal Verification], Berkeley University of California, Retrieved November 6, 2013</ref>