AI BriefingBasis Research Proves LLM-Generated Semantics for a Small Language Match Its Compiled Interpreter's RISC-V Execution
·2026.10.16 09:00
Key point
Basis Research used LLMs to write formal semantics for an extended WHILE language and prove in Lean that its compiled C interpreter's RISC-V binary execution matches those semantics.
Details
- The team verified an extended version of the WHILE language, using a 1,855-line C interpreter compiled to 25,336 RISC-V instructions.
- The proof process involved porting separation logic to Lean to handle memory allocation, reducing the final proof size to under 200,000 lines from an initial peak of 1 million.
- The verification identified implementation details such as 63-byte closure name truncation that were not captured in initial semantic drafts, while 64-bit integer wrapping was part of the defined language arithmetic.
- Derived tools including a type checker, program logic, abstract interpreter, and verified compiler were developed, with the compiled code retiring 2.7 to 8.2 times fewer instructions than the interpreter on a RISC-V simulator.
- The team has stated headline theorems for extending this approach to Lua 5.4.7 and OCaml, with CPython identified as the long-term goal, though the proofs for the new languages remain to be closed.
This summary was generated automatically by AI. Check the original for the author's claims and context. Copyright belongs to the original author.
Our guide explains how the AI works. Report summary errors, attribution issues, or removal requests via Contact.
Related
Terence Tao Proposes 'Math 2.0' Framework to Shift Mathematics from Proof Scarcity to Proof Abundance
New Paper Argues Lean Verification Fails to Guarantee Correctness of AI Autoformalised Navier-Stokes Proof