seL4 is about 9000 LOC. So this gives a good indication of what formal verification (Isabelle/HOL) is currently capable of. seL4 is also quite fast as a result of removing unnecessary checks.
Note that this is formal verification of an imperative, C-based program manipulating low-level structures done years ago. I wouldnt say that represents what we're currently capable of in general case. For starters, a functional program or imperative without pointers (eg in SPARK) is much easier to verify than a C program. Plus, the seL4 organization recently reduced effort for filesystems down by a few multiples with a functional language.
Truth is the seL4 team set themselves up for a harder-than-usual job. For good reason but most folks (esp managed languages) won't see as much difficulty.
I want to learn formal verification on my own. Do you know of any resources? I got Rolf Dreshler's book on circuit verification, but I would like to master both hardware and software. Would you kindly provide with some pointers?
It's a broad subject and I'm only interested in software verification. It's specialized enough that you should be reading papers and reading about systems. My favorite systems+papers are:
* Coq/dependent types. Check out Software Foundations by Benjamin Pierce, et. al. Everything's online. Also see Idris, which has a good book from Manning.
* SMT-solver-based verification of existing languages. See SPARK/Ada (there's a good book but I can't remember the name presently) and the GNAT website. Also, Frama-C, although the documentation is more spotty. Then there's Rustan Leino's work on Dafny and Boogie. Oh, and Why3. And some work on verifying Java code that I haven't played with yet.
* Model checking/high level formal specs. Lamport's TLA+, Alloy, possibly Z. There are some good TLA+ things online, I just couldn't get into it. (I feel bad.)
As far as I know, Isabelle/HOL is fairly similar to Coq, perhaps with more automation. If there is something like Software Foundations for Isabelle, I'd be slobbering all over myself in excitement to hear about it.
(And I'm still a little confused about how the C code of seL4 is verified against the formal specs. Is there something like Frama-C involved?)
Both are interactive theorem provers, so yeah. But the two school comment said Coq/dependent-types, and Isabelle/HOL is neither Coq, nor does it do dependent types :)
https://www.sigops.org/sosp/sosp09/papers/klein-sosp09.pdf
seL4 is about 9000 LOC. So this gives a good indication of what formal verification (Isabelle/HOL) is currently capable of. seL4 is also quite fast as a result of removing unnecessary checks.
https://sel4.systems/
seL4 is smaller than L4Ka::Pistachio and it's also capability based which L4 isn't. They could have called it L5 or seL5.