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 certi

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).