> how do you prove that the formal spec correctly describes what the software's supposed to do? This is a valid point. With formal verification, the buck stops

> how do you prove that the formal spec correctly describes what the software's supposed to do? This is a valid point. With formal verification, the buck stops with the model. Looking at existing projects like Sel4, though, it's clearly not a knock-down argument against formal methods. > Your proof that it has no null pointer crashes tells us nothing about whether it has off-by-one errors. For each kind of bug, you need a different proof. Did your proof cover every category of bug? Almost certainly not. This appears to be a guess at how formal methods work. It is wrong. Formal methods are able to take an abstract model and 'refine' it into an executable program that implements the formal model. [0] This process is mathematically watertight (ideally at least). There is no room for language-specific bugs (such as buffer overflows) to creep in. What you don't tend to get from formal methods, is a guarantee against side-channel attacks, such as timing-based attacks. This may be a real security concern. From a quick google search, this seems to be an active area of research. [0] https://en.wikipedia.org/wiki/Refinement_(computing) https://en.wikipedia.org/wiki/Refinement_(computing)