Book-Guided, LLM-Detailed, Kernel-Verified: Formal Proof Construction from ZFC Axioms to Program Correctness

We present a formal proof development building from ZFC set-theory axioms to a verified Turing machine program, guided by a textbook and detailed by an LLM, with all 246 theorems checked by a 622-line C proof kernel. The flagship result proves that a 5-state unary addition. The system uses a custom pure-functional proof language (.min) with persistent caching, achieving a clean kernel/userspace separation where the kernel guarantees soundness independent of the LLM. Source: https://github.com/yuchenkan/min