Basis makes LLMs prove their language rules match the real interpreter

Ship Your Interpreter

Basis researchers had LLMs write formal semantics for a small language, then used Lean to prove the rules match a C interpreter compiled to RISC-V for every program. Testing alone missed a real bug: the semantics ignored a 64-byte buffer limit in stringifying functions, so long names broke. The proof forced the fix. The full development is on GitHub.