Basis proves LLM-written language semantics against a compiled RISC-V interpreter

What the team did

Researchers at Basis report an experiment in which large language models wrote a formal semantics — a set of precise mathematical rules defining how a programming language behaves — for a small imperative language, and then used the Lean proof assistant to show that those rules agree with the language's actual implementation down to machine code.

According to the Basis blog post, titled "Ship Your Interpreter" and written by Kiran Gopinathan, Nikhil Pimpalkhare, Yiyun Liu and Zenna Tavares, the target is an extended version of WHILE, the textbook imperative language. Their version adds integers, strings, first-class functions with closures, if, while and for loops, and runtime errors, with 64-bit wrapping arithmetic for integer operations. The interpreter is 1,855 lines of C, and an LLM produced roughly 400 lines of Lean rules describing the language, one rule for each kind of expression and statement.

The interpreter as the authority

The team's method treats the shipped interpreter as the authority on what programs in the language mean. They compiled the C interpreter to RISC-V, an instruction set that already has a formal specification, producing an exact though hard-to-read account of what the interpreter does with any program. The LLM agents then had to prove in Lean that their readable rules predict exactly what the compiled interpreter prints for every possible program. If a rule is wrong, the proof cannot be completed — the process stalls rather than silently passing. Basis says the full development, semantics and proof together, has been published on GitHub.

Why the test suite was not enough

The post explains why that proof step matters. An early version of the generated semantics passed the interpreter's entire test suite yet still disagreed with the compiled binary in one case: when a function's name reached 59 characters, the binary truncated the name in its printed output while the semantics printed it in full. Testing missed the divergence entirely; a proof checked against the binary cannot, because any mismatch blocks the proof from going through.

Part of a larger push

Basis frames the experiment as one step toward verification that could plausibly cover all software. The post recounts that in April its agents built a JavaScript-to-WebAssembly compiler but could not prove it preserved program behaviour; months later the agents verified Linux's nftables compiler, which translates firewall rules into instructions the kernel executes. In September, MIT researchers Frans Kaashoek and Nickolai Zeldovich used AI agents to verify the xv6 teaching operating system down to its machine code.

The wider obstacle is that formal semantics exist for only a handful of languages — CompCert for C, CakeML for ML, JSCert for JavaScript, plus the RISC-V instruction set — and each took years of expert work, often covering only a subset of the language. Most languages have none, leaving nothing precise to prove programs against. Basis argues that as LLMs improve at constructing proofs, the hard problem is moving to specification: making sure the statements being proven capture the behaviour people actually care about.

Why it matters

Machine-checked proofs eliminate whole categories of bugs rather than sampling for them, and Basis's stated motivation is explicitly adversarial: LLMs are becoming markedly better at locating and exploiting bugs in production software, and verified software is one of the few defenses that keeps pace.

The specific technique here — deriving a language's formal semantics from its existing interpreter, with the proof checked against compiled machine code rather than tests — offers a route to rigorous, machine-checked definitions for languages that never had one. That is a prerequisite for verified compilers, interpreters and analysis tools built on top. The open question is scale: this experiment covers a small textbook language, not a production one, and whether the same pipeline holds up against the surface area of real languages remains to be shown.