
L'écriture des 7500 lignes de code a nécessité 4 ans, la preuve est composé de 10.000 théorèmes et de 200.000 lignes de preuves.
L'utilité de ceci est d'être sûr que certaines failles classiques ne peuvent être exploités.
Vous en pensez-quoi ?
Plus de détails sur le projet : http://www.ertos.nicta.com.au/research/sel4/