With formal verification, you make a specification, and then prove that your program adheres to the specification as written. This is usually done with a proof assistant to ensure the proof is sound. The sel4 microkernel is a good example. The kernel is written in C, but the specification and proofs are written in Isabelle, a proof assistant.
Specification and proofs: https://github.com/seL4/l4v
The microkernel itself: https://github.com/seL4/seL4
The main practical difference between testing and formal verification is that testing alone cannot guarantee correctness, i.e., the absence of errors in a program; it can only reveal errors, with no guarantee of revealing all of them. The only way to prove correctness is to write a proof of adherence to a specification.
I found a good example of this from an excerpt of the book Program Construction by Roland Backhouse. The code is in Pascal.
The problem the students had been set was to write a program that would compare two strings for equality. One student's solution was to assign the value true or false to a boolean equal as follows:
equal := (string1.length = string2.length)
if equal
then for i := 1 to string1.length
do equal := (string1.character[i] = string2.character[i])
The student was quite taken aback when I demonstrated the error. Indeed, upon further questioning, it emerged that the program had been tested quite systematically. First, it had been tested on several pairs of identical strings, and then on several pairs of strings of unequal length. Both these tests had produced satisfactory results. The final test had been to input several pairs of equal length but unequal strings, such as 'cat' and 'dog', or 'house' and 'river'.
This final test is interesting because it is possible to use simple probability theory to make a rough estimate of the chances of discovering the programming error. The details are not relevant here. Suffice it to say that, assuming pairs of words of equal length are generated with equal letter frequencies (that is, each letter in the alphabet is chosen with a probability of 1/26), there is only a one in three chance of discovering the error after ten tests; increasing the number of tests to 20 would still only yield a one in two chance, and one would need to perform over 50 tests to achieve a 90% chance of discovering the error. Finally, and most importantly, there is no certainty that one would ever discover the error, no matter how many tests have been performed.
This is a great illustration of how testing can't guarantee correctness. It's easy for someone who isn't a beginner programmer to see why the code is incorrect, but it wasn't obvious to the student; this shows that, like the beginner, if you ever write code that is hard for one of your skill level to write, and which is subtly incorrect, you may never actually realize it without extensive testing, and if it's not extensive enough, you may still never find the bug.
Open source variants include the more well-known seL4 [3] and L4Re [4].
The L4 family is known for formal verification of significant parts of the system, and is used in safety-critical systems [5].
Google recently announced a system based on seL4 [6].
[1] https://sigops.org/s/conferences/sosp/2013/papers/p133-elphi...
[2] https://docs.sel4.systems/projects/sel4/frequently-asked-que...
[3] https://github.com/seL4/seL4
[4] https://github.com/kernkonzept/l4re-core
[5] https://www.youtube.com/watch?v=ijTTZgQ8cB4
[6] https://opensource.googleblog.com/2022/10/announcing-kataos-...
All of this is incredibly difficult, and an open area of research. Probably the biggest example of this approach is the Sel4 microkernel. To put the difficulty in perspective, I checkout out some of the sel4 repositories did a quick line count.
The repository for the microkernel itself [0] has 276,541
The testsuite [1] has 26,397
The formal verification repo [2] has 1,583,410, over 5 times as much as the source code.
That is not to say that formal verification takes 5x the work. You also have to write your source-code in such a way that it is ammenable to being formally verified, which makes it more difficult to write, and limits what you can reasonably do.
Having said that, this approach can be done in a less severe way. For instance, type systems are essentially a simple form of formal verification. There are entire classes of bugs that are simply impossible in a properly typed programs; and more advanced type systems can eliminate a larger class of bugs. Although, to get the full benefit, you still need to go out of your way to encode some invariant into the type system. You also find that mainstream languages that try to go in this direction always contain some sort of escape hatch to let the programmer assert a portion of code is correct without needing to convince the verifier.
[0] https://github.com/seL4/seL4
word_t strnlen(const char *s, word_t maxlen)
{
word_t len;
for (len = 0; len < maxlen && s[len]; len++);
return len;
}
https://github.com/seL4/seL4 (from file src/string.c)
"The world's first operating-system kernel with an end-to-end proof of implementation correctness and security enforcement is available as open source."
for instance, look at strnlen:
word_t strnlen(const char *s, word_t maxlen)
{
word_t len;
for (len = 0; len < maxlen && s[len]; len++);
return len;
}
for example there are a few ways to count the lines of code of sel4[1] kernel maybe 10,000 lines, maybe 60,000 lines.
But to gauge it vs the linux kernel both 10k vs 20m and 60k vs 20m both give you the orders of magnitude to make a good comparison.
> They find issues in libCURL and openSSL that have existed for years
Neither of them are formally verified. https://github.com/seL4/seL4 however is formally verified.
Homepage: https://sel4.systems/
Github: https://github.com/seL4/seL4
Related course (already posted on HN i think but can't find its associated thread): http://www.cse.unsw.edu.au/~cs9242/14/lectures/