4 ms·
As far as I know, The seL4 microkernel team generates C code by hand from a formally-verified "executable specification" written in Haskell. Which is then veri
by hga 10y ago
As far as I know, The seL4 microkernel team generates C code by hand from a formally-verified "executable specification" written in Haskell.
Which is then verified by analyzing the binary code and linking it back to the spec.