Comment by AstralStorm
2 days ago
This is the case for formal proofs. You can even generate V code from them, much like SEL4 is written.
2 days ago
This is the case for formal proofs. You can even generate V code from them, much like SEL4 is written.
A formal proof isn't sufficient on its own for safety-critical applications. You also need to show that your assumptions actually hold in the system and that your proof is the right proof for that system.
I usually tell people that safety-critical processes aren't really about eliminating bugs, that's just a happy side effect. They're about ensuring that the risks for the system are known and reasonably mitigated, with documentation to prove it.