CoqToLeanAsm: x86 Macro Assembler in Lean 4

2.2. Game of Life on Bare Metal (Paper Figure 2)

The paper shows Conway's Game of Life running on bare hardware—no operating system. By appending a boot loader and creating a CD image, the Coq-assembled code boots directly in a virtual machine. This demonstrates that the assembler produces real, executable machine code, not just a model.