In a previous blog post, we talked about formal verification and how we can convince ourselves (and others!) that a piece of software really works as intended. Now that we have managed to complete formal verification of our first component, the keystore, I would like to talk about it in more detail.

First of all, it is important to note that formal verification is not at all like the standard method of ensuring that software works – testing. Rather than running a program with all possible inputs and checking that the output is what we expect, formal verification is more like printing out the source code and going through it with a fine-tooth comb to make sure it does what it is supposed to and does notcontain any bugs.

If we really did it that way, the process would be pretty error prone, but we have a piece of software called an interactive theorem prover that checks our reasoning for us to make sure it is valid and we have not forgotten anything. We still must write the proof ourselves, but the theorem prover makes sure the proof is correct. (For this to work, the theorem prover must have some idea of our programming language – it has to know exactly what each statement in the source code does!)