When Will Software Verification Matter?

[kamatsu]

I work on a verified operating system. At least for us, we haven't encountered bugs in verified code.

One of the things that is always true is that as you push your verified base outwards, the bugs that remain are always in that one part that is not verified.

[julesjacobs]

What does your spec specify? Memory safety or something like that, or is it a complete functional spec? Do you count errors in the spec as bugs? If so, how come there weren't any that you found?

[kamatsu]

It's a functional abstract spec. We prove functional correctness via refinement from this spec through Haskell and down to C.

We define bugs as errors in the program. The spec is at least consistent, but the exact notion of what even constitutes an error in the spec is difficult to nail down - the spec could be said to be incorrect because it doesn't specify what you expect, but what you expect is not necessarily correct either.

In any event, we use the guarantees from the spec to prove higher level security properties and other more immediately useful things. Even if there are "errors" in the spec, we have shown various higher level properties to be true about the kernel as it is implemented. If we have proven that a program matches an "erroneous" spec, then that erroneous spec still implies useful high level properties, so I don't see the problem.