[erichocean]

The entire QK[1] kernel, including all library code, is less that two thousand lines of C (and most of the library code isn't even used by the kernel itself, which is just 234 LOC). QK is a single-processor kernel (although still pre-emptive) and very well written and tested (in, literally, hundreds of millions of devices).

It was not difficult at all to run QK and it's supporting code through KLEE and exhaustively verify the properties of each function, thanks to a super-simple design and the many included assertions, preconditions, and postconditions, which KLEE helpfully proves are satisfied automatically. If I wanted a certified optimizing C compiler, I'd use CompCert[2] to compile QK, which would give me a certified kernel all the way to machine code. (I actually use Clang.)

I am familiar with the verified L4 kernel, and it is far more complex than the QK kernel I have verified. That people have already verified a kernel far more complex should be sufficient proof that a much simpler kernel can also have its correctness verified.

Stepping back, it's 2012: people should no longer be surprised when a small-but-meaningful codebase is certified correct. It's common enough now that you don't get published in a journal just because you did it.

[1] http://www.state-machine.com/qp/index.php

[2] http://compcert.inria.fr/

[javert]

By the way, I am going to look into actually applying KLEE to some of my own code. I had heard of it before, but thanks for bringing it up, I hadn't really given it much thought until now.

In my research, I'm trying to write a "fancy" task scheduler at the user level, so that someone can get "fancy" scheduling policies without modifying the RTOS kernel. By "fancy" I mean fully preemptive and allowing "interesting" scheduling policies/synchronization protocols to be implemented. "Interesting" generally means multicore, in my particular research community.

If you don't mind me asking, what kind of projects do you/have you used QK for?

[javert]

Interesting. I had never heard of QK, and I'm slightly surprised about that.

people should no longer be surprised when a small-but-meaningful codebase is certified correct

For the size of codebase you're talking about, I'm not really that surprised. But I still think that formal methods don't scale to multicore RTOSs, which is the area I study (I'm a CS grad student).