Hacker Newsnew | past | comments | ask | show | jobs | submitlogin

I'm not sure you are aware, but formal verification[1] is a well known and respected field of research. It does work, but it is hard to build practical tools using it. Nevertheless, if something is formally proven correct then for it to be incorrect one of three things must happen:

1) The proof is incorrect (which of course means it is no longer proven)

2) The prover has a bug (most proofs are done automatically). This is possible, but many of the same formal methods are used on the prover, and it is often build on a human-proved proof at the bottom.

3) Mathematics (the whole field) is wrong. This seems unlikely.

In reality, the problem with formally verified software is generally that it must interact with non-verified software (and sometimes hardware - although hardware can be verified too).

The wikipedia page[1] I referenced is worth reading.

[1] http://en.wikipedia.org/wiki/Formal_methods



The prover has a bug (most proofs are done automatically).

Minor point: while many formal verification projects are proven automatically, seL4 is proven in Isabelle/HOL which is an interactive theorem prover. This means that the proofs are actually carried out mostly manually. (The downside is that it takes much longer to carry out proofs; the upside is that you can prove far more sophisticated properties than is possible with the current state-of-the-art automated provers).

You are still right that the proof checker could have a bug, though. Proof checkers tend to be much smaller and simpler than things like SMT solvers, which helps increase confidence in them, however.


4) It meets the specification but the specification is incorrect/specifies sub-optimal behaviour.


If you can fix that problem in the general case then you are about to be a very, very rich person.




Guidelines | FAQ | Lists | API | Security | Legal | Apply to YC | Contact

Search: