|
|
|---|
|
|
|
|---|
Jitawa is a Lisp runtime developed by Magnus Myreen that is capable of running the Milawa kernel and checking through the entire bootstrapping process, and which is verified down to the machine code with HOL4.
Magnus Myreen has used the HOL4 system to prove an unbelievably impressive theorem: if you run the simplified Milawa kernel on his Jitawa Lisp runtime on an 64-bit X86 system, it can only accept theorems of formulas that are semantically true. This theorem connects the logical semantics, down through the kernel's source code, through the Jitawa Lisp implementation, down to a formal HOL model of the x86 machine code!
The best source of information about Jitawa and these HOL4 proofs is Magnus' Jitawa page. You may also be interested in the following papers and slides.