and documentation about it:
Jorge tells me that there is this guy at NICTA who came up with the L4 microkernel implementation using the B-method:
So having that on the table why not having a zero defect thesis, as b-core promises?
The B Method, developed by Jean-Raymond Abrial , is a system of formal development from the initial high-level speciﬁcation all the way to implementation via a process called reﬁnement. It is one of the few formal methods to do so. The idea is to abstract away the implementation and concentrate on pure functional requirements at the top level. Then, with each reﬁnement step, provide more information on how exactly the system fulﬁls those requirements, until enough information exists to implement the system. Each reﬁnement step requires proof of consistency with the previous step.