[cliffu]

I vote yes. Formal verification has great benefits for software security and it's the "final form" (if you will pardon a redditism) of unit testing. It's one of the top skills I would like to learn.

You might be interested in L4; there's a variant that has been formally verified (but I think it's closed source?).

[MichaelSalib]

Formal verification allows you to prove that an implementation faithfully implements its specification. What does the formal specification for a web browser look like? I'm guessing that we're talking about thousands of pages of extremely dense math and code. How do you know that that specification is correct, or reasonable or what the user wants?

Now, maybe we don't want to do formal verification for correctness because it is too hard. So we settle for formally verifying that a program has some property of interest, like memory safety. But if you want memory safety, it is a lot cheaper to just use a language that gives you memory safety for free (haskell/scala/go/python) rather than trying to formally verify that your C++ program is memory safe.

[mokus]

> You might be interested in L4; there's a variant that has been formally verified (but I think it's closed source?).

You are probably thinking of seL4[1] unless there's another I don't know about. I believe you are correct that it's closed-source. That always bugged me though, since it seems to defeat the whole purpose of verifying such a critical part of a system's TCB. In my mind, the whole point is that I as a user don't need to just take anyone's word for it.

Unless I'm mistaken (and I'd love to find out that I am!), what we have with seL4 is a commercial vendor handing out an opaque binary blob and saying "we proved it's correct!" but providing no way for the user to verify that they really did prove anything. Frankly, these days I just don't trust any organization's assertions on such things no matter how thoroughly they claim they have proved it _to themselves_. It's certainly better than "we hit it with a hammer and it didn't break, most of the time!", but it still leaves open the possibility that the person asserting it's proved is lying, or that they did prove it's correct _except for the backdoor the NSA secretly coerced them into adding to the version they released_.

I wish I had the time to tackle something similar for the open-source world, but with 2 small kids around I barely have time for the small open-source projects I do manage. It's very cool too see this article's work being released in source form, and I really hope some open-source devs pick it up and run with it. I for one hope to be able to contribute in what time I do have.

[1] http://www.ertos.nicta.com.au/research/sel4/