Jitawa — a verified Lisp runtime for Milawa. This page contains source code, documentation and proofs scripts relating to a verified Lisp runtime, called Jitawa. Jitawa was designed to host Jared Davis’ Milawa theorem prover — a prover which we have formally proved to be sound when run on Jitawa.

Keywords for this software

Anything in here will be replaced on browsers that support the canvas element