Computer Assisted Proofs

Formal verification, a rapidly growing young field, is the computer assisted proving of results - ordinary mathematical theorems, as well as claims that pieces of hardware or software, network protocols, and mechanical and hybrid systems meet their specifications. Computers can assist both in the discovery of proofs as well as checking correctness. Indeed computer assisted finding of proofs (so called Automated Theorem Proving) is crucial for formal verification of any complex result or system, as manually supplying all details of complex proofs can be hard and tedious.

Formal verification offers an assurance of correctness far beyond other forms of testing. However, it is not easy to develop such proofs, so we have to weigh the benefits of safety against the cost of the extra effort (and the consequent loss of productivity). In recent times, our ability to develop such proofs has greatly increased (thus lowering the cost), and the importance of the greater safety from proofs, especially in some domains, has greatly increased. Together these make a compelling case for increasing use of formal verification.

Who guards the guards?

If the system that checked our proofs is wrong, then we naturally cannot be sure of the correctness of the proofs, so on the face of it we are left with human verification of a piece of software (the formal proof system) instead of proofs. This issue is mitigated by following trusted kernel principle - the kernel is a separate program that checks the correctness of proofs. The kernel can be of moderate size (since it only needs to check, not find, proofs), and can be rigorously reviewed and tested. An excellent implementation of this principle is with the Lean theorem prover - the proofs are exported to an easy to read format, and there are three independent programs, written in three different programming languages, that check proofs. Further all these proof-checkers are open sourced and of moderate size.

The necessity and value of proofs

Traditionally systems undergo various kinds of tests that ensure that they fail only very rarely. However, there are circumstances where even such rare failures are not acceptable.

As systems become increasingly complex, and the mathematical and scientific literature grows, traditional ways of checking such as statistical testing and reviews by other people (including of human mathematical proofs) become increasingly inadequate in ensuring correctness.

Further, proofs not only establish correctness of results, but illuminate them. Specifically, the act of formally proving a result makes clear what assumptions go into this result, both clarifying its scope and potentially leading to further advances in knowledge.

How to prove it

Many advances have come together to make formal verification feasible.

These advances work together - better provers make it easier to add to the libraries, which in turn strengthen provers. Further as each component grows stronger, it increases the value of the other components, and hence the resources invested in it.

The road ahead

Many future advances will come from conceptual and technical advances in foundations and provers and growing libraries of formalized results. There are also approaches with great potential that have not yet been incorporated in a significant way.

As formal verification grows in power, one can hope to use this in many other areas and to a much greater extent. For instance, people are working on formal verification of cryptographic protocols. There are also efforts to make formal verification practically useful in some areas of mathematics.

Yet, this is a young field with a small community working in it, so the potential for making significant contributions at this stage is high. And one can hope that the value of these contributions grows as automated theorem proving and formal verification become more widespread.