B->AMN

Abstract machine notation, I meet with a friend of mine, "tocayo" Jorge Eduardo Cardona and between beers, he told me about this thing he was reading, the B-method, so it came in to my curiosity todo reading list, and as i got to talk to him tody again i remembered, I found this site:
http://www.b-core.com/aboutb_method.html
and documentation about it:
http://www.b-core.com/ONLINEDOC/Contents.html
Jorge tells me that there is this guy at NICTA who came up with the L4 microkernel implementation using the B-method:
http://cgi.cse.unsw.edu.au/%7Erafalk/pubs/b-l4-api.pdf
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 [1], is a system of formal development from the initial high-level specification all the way to implementation via a process called refinement. 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 refinement step, provide more information on how exactly the system fulfils those requirements, until enough information exists to implement the system. Each refinement step requires proof of consistency with the previous step.

Rafal Kolansk