Formal verification of software.


The [seL4]( microkernel had been “formally verified”, which I understand to mean that it has been mathematically proven to work as intended in every single situation. How does one even go about this? What is the procedure for formally verifying a piece of software and how difficult is it, and does it only require formal verification of the software itself or the compilers and programming languages that created the program as well?

And if you ever update the software, does the formal verification become invalid?

In: Technology

When you write the software, you have to define in a narrow mathematical way, what it must do. Then you can combine a combination of formal theorem proving software and carefully designed experimental testing. Many specialized tools, including compilers and other development tools are used. Most L4 kernels are written in C++, though I don’t know for sure about seL4.