Things change, computer dev evolves too openbsd dev team uses audit code with great success but many industrial domains uses new technics like static analysis with success too for exemple in avionics soft : astrée is a tool that certified Airbus plane software with static analysis read astree web page <http://www.astree.ens.fr/>
in such domain perfection could not exist : church gödel turing in 1930 ... but it could be interesting for the core team to have a static analysis tool to test OpenBSD kernel code it will not be a simple task for sure but it's for my own opinion a necessity and keep openBSD far beyond ... some researchers still have this in mind ... openbsd superlint<http://kindsoftware.com/documents/proposals/superlint.html> in short and private joke : openbsd, (model) checks your 6 ! ... (release) ;) Iki