Comment by mrheosuper
2 days ago
> How do we get to a point to `trust` it?
You don't, similar to you don't trust code written by human. The code needs to be audited, line-by-line.
2 days ago
> How do we get to a point to `trust` it?
You don't, similar to you don't trust code written by human. The code needs to be audited, line-by-line.
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.
Audited by ?
Redundant verification processes. Think swiss cheese model. No system is perfect, so you layer independently imperfect systems to avoid catastrophic failures slipping through the cracks.