{"article":{"slug":"ship-your-interpreter","title":"Ship Your Interpreter","subtitle":null,"summary":"Basis researchers show how LLMs can invent a programming language, write an interpreter, and prove that the interpreter follows the language's rules—arguing that shipping a verified interpreter is becoming a practical unit of AI-generated software, not just generated code snippets.","content_type":"research","language":"en","canonical_url":"https://www.basis.ai/blog/ship-your-interpreters/","author":{"name":"Kiran Gopinathan, Nikhil Pimpalkhare, Yiyun Liu, Zenna Tavares","url":null,"person_slug":null,"person_url":null},"authored_by":"human","publisher":{"name":"Basis","url":"https://www.basis.ai","listing_slug":null,"listing":null},"topics":[{"name":"AI","slug":"ai","url":"https://listedarticles.com/topics/ai"},{"name":"Programming","slug":"programming","url":"https://listedarticles.com/topics/programming"},{"name":"Research","slug":"research","url":"https://listedarticles.com/topics/research"},{"name":"Software Engineering","slug":"software-engineering","url":"https://listedarticles.com/topics/software-engineering"},{"name":"LLMs","slug":"llms","url":"https://listedarticles.com/topics/llms"}],"about_listings":[],"cover_image_url":null,"license":"all-rights-reserved","word_count":4264,"reading_minutes":19,"published_at":"2026-10-16T00:00:00.000Z","added_at":"2026-10-17T17:18:51.858Z","updated_at":"2026-10-17T17:18:51.858Z","added_via":"api","contributor":{"type":"agent","name":"ListedStartups Using Bot","registered":true},"profile_url":"https://listedarticles.com/articles/ship-your-interpreter","markdown_url":"https://listedarticles.com/articles/ship-your-interpreter.md","example":false,"citation":"Kiran Gopinathan, Nikhil Pimpalkhare, Yiyun Liu, Zenna Tavares, Basis. \"Ship Your Interpreter.\" 16 Oct 2026. https://www.basis.ai/blog/ship-your-interpreters/ (all-rights-reserved)","access":{"human_view":"preview","full_text_available":true,"source_url":"https://www.basis.ai/blog/ship-your-interpreters/"},"body_markdown":"We had LLMs write precise mathematical rules, or a formal semantics, for how a small programming language should behave. We then used Lean, a tool for checking mathematical proofs, to prove that the interpreter—the program that runs code written in that language—follows those rules even after being compiled into low-level instructions understood by a RISC-V computer chip.\n\n![](https://www.basis.ai/ship-your-interpreters/pipeline_v1.svg)\n\nLLMs are growing alarmingly capable at finding and exploiting bugs in\nproduction software, with increasing reports of AI-assisted hacks\nin the wild.\nFortunately, LLMs are advancing quickly in their ability to write\n*verified software*: programs that come with mathematical proofs,\nchecked by a computer, that rule out entire classes of bugs.\nIn April, our agents [built a JavaScript-to-WebAssembly\ncompiler](https://www.basis.ai/blog/verified-compiler/) but could not prove that it preserved\nprogram behaviour. Months later, our agents [verified Linux’s nftables\ncompiler](https://www.basis.ai/blog/verified-nftables/), which translates firewall rules\ninto instructions the kernel executes. In September, MIT researchers\nFrans Kaashoek and Nickolai Zeldovich used AI agents to [verify the xv6\noperating-system kernel](https://arxiv.org/abs/2609.04043) down to its\nmachine code.\n\nOur goal at Basis is to develop verification methods that could plausibly scale to all software, so that the systems powering critical infrastructure are secure by design and keep pace with attackers’ growing capabilities.\nAs LLMs advance in capability, the bottleneck is shifting away from theorem proving and towards the problem of specification: how can we be sure that the statements we prove capture the behaviour we actually care about?\n\nTo prove anything about a program, we first need a mathematical description of what it does.\nThis starts with describing the programming language it is written in: what every statement, loop, and function call means when it runs.\nThese descriptions are called a *formal semantics*, and can be written with pen and paper, but are increasingly expressed in a proof assistant such as Lean.\nA handful of languages have one (Standard ML, WebAssembly, and C via CompCert), as does the RISC-V instruction set that a growing number of processors execute.\nDeveloping each of these semantics took years of expert effort.\n\nMost programs, however, are written in languages that do not have a formal semantics, presenting a major bottleneck for deploying verified software at scale: without a semantics, there is nothing precise to prove against.\nA natural solution is to use LLMs to write semantics, but LLMs make mistakes, and a broken semantics undermines every proof built on it.\nTesting helps, but as we show below, a semantics can pass every test and still be wrong. What is needed is a means to verify the semantics itself.\n\nLanguages without a formal semantics still have interpreters or compilers, which in practice define what their programs mean.\nHere we consider a radical idea: make the LLM prove that its semantics agrees with the real interpreter on every program, treating the interpreter as ground truth. To do this, we compile the interpreter to RISC-V, whose meaning is already formally defined. That gives an exact, if unreadable, description of what the interpreter does with any program. The LLM then writes readable rules for the language and proves in Lean that, for every possible program, those rules predict exactly what the compiled interpreter prints. If a rule is wrong, the proof gets stuck.\n\nWe report on an experiment where we had LLMs develop a semantics and\nits proof together for a small language. We used Lean to prove that the interpreter, the\nprogram that runs code written in that language, follows those rules\neven after being compiled into low-level machine instructions. The\nwhole development, semantics and proof, is\n[on GitHub](https://github.com/BasisResearch/ship-your-interpreter).\nThe rest of this post walks through this\nexperiment, explaining first why semantics are the bottleneck for\nlarger verification efforts and why tests aren’t sufficient to build\ntrust in them. We then show how the proof process refined the semantics,\nhow we handled the memory reasoning, and what tools we built on the result.\n\n# Every verified program starts from a semantics\n\nBefore you can prove a program does anything, you have to define how\neach operation transforms its state, that is, define its *semantics*.\nMost languages describe their semantics informally in prose, in a\nreference manual, and leave the concrete details to the compiler or\ninterpreter implementation. A *formal*\nsemantics writes the rules down in mathematics, precisely enough for a\nproof checker like Lean 4 to use them. Notable examples include\nCompCert’s semantics for C, CakeML’s for ML, and JSCert’s for JavaScript.\nEach one took years of expert effort, and often covers only a restricted\nsubset of its language.\n\nFor this experiment we used an extended version of WHILE, the small\nimperative language used in textbooks such as Nielson and Nielson’s\n[*Semantics with Applications*](https://orbit.dtu.dk/en/publications/semantics-with-applications-a-formal-introduction/).\nOur version has integers, strings, first-class functions with closures, `if`, `while`\nand `for` loops, and runtime errors. Its interpreter is 1,855 lines of\nC, and a WHILE program looks like this (it prints 55):\n\n```\nvar i = 0;\nvar sum = 0;\nwhile (i < 10) {\n i = i + 1;\n sum = sum + i;\n}\nprintln(sum);\n```\n\nThe semantics an LLM wrote for WHILE is a set of rules, one for each\nkind of expression and statement. These rules describe how to evaluate\nan expression in terms of its subexpressions. For integer addition,\nthe rule is:\n\n```\nst, env ⊢ l ⇓ a, st' st', env ⊢ r ⇓ b, st'' a + b = c\n──────────────────────────────────────────────────────────\n st, env ⊢ l + r ⇓ c, st''\n```\n\nA rule reads from the bottom up. The line at the bottom is its\nconclusion. Starting from state `st` in environment `env`, the\nexpression `l + r` evaluates (`⇓`) to `c` and leaves state `st''`.\nThe state holds variable values, closures and everything printed so\nfar; the environment says which variables are in scope. The premises\nabove the line explain how the result follows from the subexpressions.\nFirst `l` evaluates to `a`, leaving state `st'`. Then `r` evaluates to\n`b` in that state, leaving `st''`. The final premise, `a + b = c`,\nadds the two integer values using WHILE’s 64-bit wrapping arithmetic.\n\nTake `(1 + 1) + x`, with state `[x ↦ 5]` and environment `{x}`:\n`x` holds 5 and is in scope. Applying the rule gives:\n\n```\n[x ↦ 5], {x} ⊢ (1 + 1) ⇓ 2, [x ↦ 5] [x ↦ 5], {x} ⊢ x ⇓ 5, [x ↦ 5]\n 2 + 5 = 7\n─────────────────────────────────────────────────────────────────────\n [x ↦ 5], {x} ⊢ (1 + 1) + x ⇓ 7, [x ↦ 5]\n```\n\nThat is, to evaluate `(1 + 1) + x`, we first evaluate `(1 + 1)` to get\n2, then look up `x` to get 5, and add the two values to get 7. Neither\nsubexpression changes the state, so `[x ↦ 5]` remains unchanged.\n\nTo justify the first premise, we apply the addition rule again:\n\n```\n[x ↦ 5], {x} ⊢ 1 ⇓ 1, [x ↦ 5] [x ↦ 5], {x} ⊢ 1 ⇓ 1, [x ↦ 5]\n 1 + 1 = 2\n───────────────────────────────────────────────────────────────\n [x ↦ 5], {x} ⊢ 1 + 1 ⇓ 2, [x ↦ 5]\n```\n\nThese rule applications form a tree that derives the value of the\nwhole expression from the values of its parts.\n\nThe LLM wrote about 400 lines of rules like these, in Lean ([the full\nsemantics](https://github.com/BasisResearch/ship-your-interpreter/blob/fb07094cff916318c34b07494a7d739f1e53989b/Vsa/While/Semantics.lean)).\nEach rule looks reasonable on its own, but an end user has no rigorous\nway to tell whether they faithfully describe how WHILE programs behave\nwhen they are actually run.\n\n# A semantics can pass every test and still be wrong\n\nThe usual way to check a semantics is to run it. Take a test suite,\nrun each program under the semantics and under the real interpreter,\nand compare what they print. Unfortunately, in practice, this process\nis insufficient to build trust in the generated semantics.\n\nFor example, an early version of our semantics passed the test suite\ngenerated for the WHILE interpreter, but disagreed with the binary\nwhen a function’s name reached 59 characters:\n\n```\nfn aaa…aaa() {} // a name of 59 a's\nprintln(\"\" + aaa…aaa);\n\nsemantics: \nbinary: `. The binary dropped the\nclosing `>`, and for longer names it dropped part of the name too.\nNo test in the suite tried functions with names this long.\n\nThe reason is in the [C\ninterpreter](https://github.com/BasisResearch/ship-your-interpreter/blob/fb07094cff916318c34b07494a7d739f1e53989b/c/src/interp.c#L80)\nthat turns a value into a string when you concatenate it with `+`:\n\n```\nstatic char *stringify(Value v) {\n ...\n char buf[64];\n switch (v.kind) {\n ...\n case VAL_FN: {\n const char *name = v.as.fn->fn_expr->as.fn.name;\n if (name)\n snprintf(buf, sizeof buf, \"\", name);\n else strcpy(buf, \"\");\n break;\n }\n default: strcpy(buf, \"\"); break;\n }\n ...\n}\n```\n\n`stringify` returns a string value as it is. Any other value is first\nprinted into a 64-byte buffer on the stack and then copied into a\nfreshly allocated string. A named closure is printed with `snprintf` as\n``, an anonymous one as ``, and the built-ins fall through\nto the default case, ``.\n\n`snprintf` writes at most 63 characters into the 64-byte buffer. The\ninitial semantics used the same rendering rule for concatenation and\nprinting, and missed this limit. To prove agreement with the binary,\nthe LLM had to give concatenation its own renderer. The\n[corrected\nsemantics](https://github.com/BasisResearch/ship-your-interpreter/commit/d0d2609425f0024a0b8a2ad0570f14723b391a8d)\ncuts a closure’s rendering to its first 63 bytes:\n\n```\n\"\" + f ⇓ take 63 (\"\")\n```\n\nThis is the kind of detail an\nimplementation accumulates internally but nobody writes down\nexplicitly, which is precisely why a semantics transcribed by hand, or\nwritten by an LLM, can miss it. Nor is it a detail no program would\nnotice: code in dynamic languages routinely relies on the string form\nof a function, for logging, for dispatch keyed on a name, or for\ncomparing serialised values. Even simple violations like\nthis undermine any verification effort built\non top of the semantics, and can leave holes that hide security\nvulnerabilities. To build secure and scalable semantics, we need to go\nbeyond tests, since a test suite only checks the programs someone (or\nan agent) thought to write.\n\n# Ship your interpreter\n\nShipping your interpreter means checking the semantics against the\nimplementation people actually run. Compile the interpreter the\nlanguage already has, and make the LLM prove that the binary\n*refines* the semantics, that is, that the two agree on what every\nprogram prints.\n\nThe theorem we\n[proved](https://github.com/BasisResearch/ship-your-interpreter/blob/fb07094cff916318c34b07494a7d739f1e53989b/VsaIris/Interp/EndToEnd.lean#L159)\nis this one:\n\n```\ntheorem endToEnd_refinement :\n ∀ p c, Loaded interpRunLayout p (fillZero c) →\n (∀ out, BigStep p out ↔ Halts c out 0) ∧\n (Diverges c → ¬ ∃ out, BigStep p out)\n```\n\nThe theorem says for any WHILE program `p`, and *any* machine\nconfiguration `c`, if the machine configuration satisfies a property\n`Loaded`, then the semantics match what the compiled binary will\ndo. `Loaded interpRunLayout p (fillZero c)` here says that `c` is a\nmachine about to run `p` through the interpreter binary. The first\nconclusion, `(∀ out, BigStep p out ↔ Halts c out 0)`, says that the\nsemantics derives output `out` if and only if the machine halts with\nexit code `0` having printed `out`, i.e. for successfully terminating\nprograms the predicted outputs are equivalent. The second says that any program\n`p` on which the machine runs forever (`Diverges c`), is a program the\nsemantics derives no terminating output for.\n\nWe can visualise this theorem as a *commuting square*, showing how the\nsemantics and the binary agree on a program’s output. In the diagram\nbelow, the top arrow relates a program `p` to the output\n`out` predicted by the semantics. The bottom arrow relates a machine\nstate `c` to the output printed when the binary halts successfully.\nThe dashed line on the left is the `Loaded` condition connecting the\nprogram to that machine state. Under this condition, the theorem says\nthe two outputs agree, shown by the double line on the right. The\norange arrow shows how a failed attempt to prove that agreement sends\nthe LLM back to revise a rule of the semantics.\n\n![The top arrow relates program p to output out through BigStep. The bottom arrow relates machine state c to out through Halts. Loaded connects p and c on the left; a double line marks equal outputs on the right. An orange arrow returns failed proof obligations to the semantics for correction.](https://www.basis.ai/ship-your-interpreters/square_v3.png)\n\nFor a program loaded into the machine, the semantics and successful execution agree on the output.\n\nThe theorem catches a wrong semantics in both directions. If the\nsemantics is too permissive, it derives an output the binary never\nprints, and the left-to-right half fails. If it is too strict, it has\nno rule for something the binary does, and the right-to-left half\nfails. Either way the LLM gets a proof obligation it cannot discharge.\nIn our experience, that obligation usually points at the rule that is\nwrong.\n\nRISC-V is an open processor design. We use its formal model, written\nin [Sail](https://github.com/riscv/sail-riscv) and translated into Lean,\nto define how each machine instruction executes. The binary is the\nactual ELF executable: 1,855\nlines of interpreter C compiled by gcc, linked against dlmalloc and\nnewlib, 25,336 instructions in all. For comparison, the xv6 kernel\nverified with MachCSL is 8,697 RISC-V instructions, built from 6,593\nlines of C and assembly, although its proof also covers concurrency,\nwhich ours does not need. The C compiler’s output, the C library and\nthe memory allocator are all inside our theorem. A person\nwho wants to trust the result reads the statement above, the hypothesis\n`Loaded`, and the two short definitions of `Halts` and `Diverges`. They\ndo not need to trust `BigStep`, because the proof checks it against the\nbinary.\n\n# Developing the semantics and proof together\n\nDeveloping the proof forced the LLMs to account for four details in\nthe semantics:\n\n- integer arithmetic had to wrap at 64 bits, because negating the\n smallest integer was unsatisfiable against the machine;\n- a `for` loop’s initialiser had to ignore an abrupt status, because\n the C does;\n- built-ins had to render differently in `print` and in concatenation;\n- long closure names had to be cut at 63 bytes.\n\nEach correction started either as an obligation that would not close\nor as a run of the binary that disagreed with the semantics.\n\nThe 63-byte cut is a representative example. The proof of the\nconcatenation case needed the semantics’ rendering to equal the\nbinary’s, and for long names it didn’t, so the obligation could not be\ndischarged until the rule changed.\n\nThe proof also caught mistakes in the LLM-generated lemmas about the C\nlibrary. The LLMs stated what each function does and then proved\nthat statement against the machine code. An allocator reserve that no\nheap satisfied after a single `malloc(24)`, a `realloc` lemma that was\nfalse for sizes that wrap, and an `exit` routine that writes `errno`\nwithout its lemma saying so all showed up the same way, as obligations\nthat would not close.\n\n# Separation logic makes the binary proof tractable\n\nLLMs wrote all of the proof. Most of the difficulty lay in reasoning\nabout memory. We needed a specification for `malloc`, the function\nthat allocates memory, which would let us prove that allocating a new\nblock preserves the data already held by the interpreter. Even\n`println(\"n = \" + x)` allocates three strings and frees two of them.\nThroughout those calls, the program’s variables and the half-built\nresult must remain intact.\n\nThe textbook way to do this is to give each function a Hoare triple\ntogether with a *footprint*, a set of bytes the function may write.\nFacts about memory outside the footprint carry across a call\nunchanged. A triple `{ P } code { Q }` reads as “if `P` holds before\n`code` runs, then `Q` holds after it”. For `malloc`, such a\nspecification reads roughly as follows, where `F` is a fixed set of\naddresses:\n\n```\n{ heap H }\n p := malloc(n)\n{ heap ((p, n) :: H) and p is fresh }\nmodifies F\n```\n\nUnfortunately, no such `F` exists. From the same heap, `malloc(32)`\nwrites the header of the new top chunk at address `0x82000238`, so `F`\nmust contain that address. `malloc(64)` instead returns the block\n`[0x82000210, 0x82000250)`, which contains it. Once the caller owns\nthat block, facts about its bytes have to survive later calls, so `F`\nmust also exclude `0x82000238`. The LLMs [proved in\nLean](https://github.com/BasisResearch/ship-your-interpreter/blob/92470bdbbfe24c8c25b5be44128aa6395e6acce8/VsaIris/DlHeap.lean#L515)\nthat no fixed set of addresses can satisfy both requirements, after a\nfirst attempt that worked around the problem one fact at a\ntime had stalled for three weeks.\n\n![Two runs of malloc from the same heap. malloc(32) writes the new top chunk's header at 0x82000238; malloc(64) returns the block from 0x82000210 to 0x82000250, which contains 0x82000238.](https://www.basis.ai/ship-your-interpreters/malloc_v2.png)\n\nFrom the same heap, `malloc(32)` writes a byte that `malloc(64)` would hand to the caller. The allocator's write footprint must change as ownership of memory changes.\n\nSeparation logic solves this by making the footprint depend on the\nheap. We ported [MachCSL](https://arxiv.org/abs/2609.04043), the logic\nbehind the xv6 proof, to the newly released\n[iris-lean](https://arxiv.org/abs/2609.24252).[1](#fn:1) In separation\nlogic the allocator *owns* the free bytes of its arena, and `malloc`’s\n[specification](https://github.com/BasisResearch/ship-your-interpreter/blob/fb07094cff916318c34b07494a7d739f1e53989b/VsaIris/DlHeap.lean#L209)\nhands part of them to the caller:\n\n```\n{ isHeap H }\n p := malloc(n)\n{ (p = 0 ∗ isHeap H)\n ∨ (isHeap ((p, n) :: H) ∗ blockOwn p n) }\n```\n\nHere `∗` is the *separating conjunction*, which says that its two\nhalves hold of disjoint parts of memory, and the result `p` is either\nnull or a fresh block. `isHeap H` owns every byte of the arena outside\nthe live blocks `H`. Initially, the allocator owns `0x82000238`, so\n`malloc(32)` may write it. If the caller instead requests `malloc(64)`,\nthat byte passes to the caller through `blockOwn`, and later calls\ncannot touch it. Anything else the caller owns is not\nmentioned in the specification, and the frame rule carries it across\nthe call in one step. After the port, the rest of the proof closed in a\nfew days.\n\n![The development in three lanes: fixed inputs (the interpreter, its binary, the Sail model, Lean's kernel), what LLMs wrote (the semantics, the representations, the separation-logic proof), and what is checked and read (boot witnesses and the refinement theorem).](https://www.basis.ai/ship-your-interpreters/pipeline_v2.svg)\n\nLLMs write the semantics and the proof linking it to the existing interpreter binary; Lean checks that proof against the machine model.\n\nAt its peak the proof was about a million lines of Lean, two thirds of\nit generated by 35 scripts the LLMs wrote, which read the binary and\nemit a proof rule for each of about 11,800 instructions. A later pass\nreplaced the generated proof families with abstractions proved once,\nsuch as a symbolic executor for machine code, and brought the proof\nunder 200,000 lines. It uses no axioms beyond Lean’s standard\nones (`propext`, `Classical.choice` and `Quot.sound`).\n\n# The theorem applies to real programs\n\nA theorem with a hypothesis is only useful if that hypothesis can be\nsatisfied. If `Loaded` described a machine state that never occurs,\nour theorem would hold vacuously and tell us nothing about the binary.\n\nWe had the LLMs [prove in Lean that `Loaded` holds for ten\nprograms](https://github.com/BasisResearch/ship-your-interpreter/tree/fb07094cff916318c34b07494a7d739f1e53989b/Vsa/Sim/Boot/Gen).\nFor each one, they constructed a machine state at the interpreter’s\nentry, with the program in memory alongside the binary, the runtime\nand the allocator. Lean checked that each state met the theorem’s\nprecondition.[2](#fn:2)\n\n![A memory map of the machine at the interpreter's entry, from 0x80000000 to 0x88000000: the ELF's code and constants byte for byte, runtime state in .data and .bss, the dlmalloc arena in its initial state holding the global frame and the AST of p, an 8 MiB stack with the interpreter object, and the registers pc, sp, gp, a0 to a3 at interp_run's entry.](https://www.basis.ai/ship-your-interpreters/loaded_v2.png)\n\n`Loaded` specifies the memory and registers needed to run the program through the interpreter binary. The program enters as a syntax tree (orange); the surrounding code and runtime state come from the interpreter.\n\nWe also replayed 85,483 machine steps from the executable and checked\nthat the resulting memory matched the constructed state byte for\nbyte. The link from the executable file and its boot trace to that\nstate was checked by scripts; Lean checked the precondition and the\nexecution from that state onwards. For the full [loop test\nprogram](https://github.com/BasisResearch/ship-your-interpreter/blob/fb07094cff916318c34b07494a7d739f1e53989b/c/tests/while.wl),\nwhich extends the earlier example with two more sums, the binary\nprovably halts after printing `55`, `2500` and `36` on separate lines.\n\nThe precondition includes enough heap and stack space for the program.\nA [later\ntheorem](https://github.com/BasisResearch/ship-your-interpreter/blob/fb07094cff916318c34b07494a7d739f1e53989b/VsaIris/Interp/EndToEndChecked.lean#L12)\nreplaces these two assumptions with checkers that run on the program.\n\n# Once you trust the semantics, the tools are cheap\n\nA validated semantics also works as an interface. Anything you prove\nsound against `BigStep` is sound for the binary, by composing it with\nthe refinement theorem, and that composition is a few lines of\nLean. So we had LLMs build four tools on top of it.\n\n![A stack: the binary on Sail at the bottom, the refinement theorem above it, the semantics above that, and four tools on top: a type system, a program logic, an abstract interpreter and a verified compiler.](https://www.basis.ai/ship-your-interpreters/tools_v2.png)\n\nThe type system, program logic and analyser reuse the interpreter's refinement proof. The compiler is proved to implement the same semantics directly on RISC-V.\n\nThe refinement proof took about a month and is about 140,000 lines of\nLean. The four tools below were opened as pull requests over three\ndays, and come to about 33,000 lines between them, most of it the\ncompiler.\n\nThe first tool is a [type\nchecker](https://github.com/BasisResearch/ship-your-interpreter/pull/5).\nIt catches invalid operations before a program runs. For example,\nthese two programs are rejected:\n\n```\n\"a\" - 1; // subtracting an integer from a string\n```\n\n```\nvar x = 1;\nx = \"s\"; // assigning a string to an integer variable\n```\n\nThe [proofs for these\nexamples](https://github.com/BasisResearch/ship-your-interpreter/blob/fb07094cff916318c34b07494a7d739f1e53989b/Vsa/While/TypeExamples.lean)\nshow that neither program can pass the checker. Its soundness theorem\nrules out type errors in accepted programs, including when they run\nthrough the interpreter binary. Division by zero, a failed `assert`\nand the interpreter’s call-depth limit remain possible; those require\nreasoning about values as well as types.\n\nThe second tool is a [program\nlogic](https://github.com/BasisResearch/ship-your-interpreter/pull/2),\nwhich lets us prove what a particular program computes. The loop near\nthe start of this post adds the integers from 1 to 10. The full [test\nprogram](https://github.com/BasisResearch/ship-your-interpreter/blob/fb07094cff916318c34b07494a7d739f1e53989b/c/tests/while.wl)\nalso adds the odd integers from 1 to 100, using `break` and `continue`,\nand computes a third sum with nested loops. The LLMs used the logic\nto prove that running this program through the interpreter binary\nterminates and prints exactly:\n\n```\n55\n2500\n36\n```\n\nThe third tool is an [abstract\ninterpreter](https://github.com/BasisResearch/ship-your-interpreter/pull/3),\nan analysis that tracks possible values through a program and raises\nalarms for potential runtime errors. It analyses that same test\nprogram with [no\nalarms](https://github.com/BasisResearch/ship-your-interpreter/blob/fb07094cff916318c34b07494a7d739f1e53989b/Vsa/AbsInt/Examples.lean),\nproving it free of runtime errors. It also establishes that the final\nvalues of `sum`, `total` and `acc` are 55, 2500 and 36. The analysis\ncomputes these results automatically, and its soundness proof connects\nthem to execution of the binary.\n\nThe fourth tool does without the interpreter entirely. In April, our\nagents built a compiler but could not prove it correct. Here the\nsemantics came first, and the LLMs built a [verified\ncompiler](https://github.com/BasisResearch/ship-your-interpreter/pull/9)\nfrom all of WHILE (strings, closures, calls, `for`, `return` and\n`assert`) straight to RISC-V. Compile the sum program above, and the\nresulting machine code prints the same three numbers. The correctness\ntheorem establishes agreement for every program meeting its\npreconditions. A [checked\nversion](https://github.com/BasisResearch/ship-your-interpreter/pull/10)\nanalyses allocation cost, so its theorem needs no assumption about\navailable heap space.\n\nDropping the interpreter also makes WHILE programs faster. We ran\nevery program in the interpreter’s test suite both ways on the\n[spike](https://github.com/riscv-software-src/riscv-isa-sim) RISC-V\nsimulator. Counting the interpreter from the moment it starts evaluating, so that\nparsing is not charged against it, compiled code retires between 2.7\nand 8.2 times fewer instructions, and both routes print the same\noutput. These are instruction counts on a simulator rather than timings\non hardware.\n\n![Paired bars on a log scale of instructions retired per test program, interpreted versus compiled: arithmetic 2.7 times fewer when compiled, strings 3.1, functions 6.5, scope 6.7, for 6.9, recursion 8.0, while 8.2.](https://www.basis.ai/ship-your-interpreters/perf_v3.png)\n\nCompiling these WHILE programs reduces instruction counts by a factor of 2.7–8.2 while preserving their output. Counts come from the spike RISC-V simulator and exclude parsing by the interpreter.\n\nOnce the semantics is trusted, it *is* the language, and the binary we\nstarted from is no longer needed to run WHILE programs.\n\n# What’s next: Lua, OCaml and, one day, CPython\n\nOur experiment with WHILE targeted a toy language. LLMs developed its\nformal semantics, proved that the compiled interpreter follows it,\nand built verified tools on top. We are now scaling this approach up\nto real languages.\n\n[Ship your Lua](https://github.com/BasisResearch/ship-your-lua)\ntargets Lua 5.4.7 compiled to bare-metal RISC-V. The binary already\nruns on the Sail model and agrees with native Lua, and the plan cuts\nthe proof at the VM: first the bytecode interpreter against a bytecode\nsemantics, fragment by fragment over opcodes, then the source language\nagainst the bytecode.\n\n[Ship your OCaml](https://github.com/BasisResearch/ship-your-ocaml)\ntakes advantage of the way OCaml bootstraps itself. OCaml’s bootstrap compiler is checked\ninto its repository as bytecode, `boot/ocamlc`, and runs on `ocamlrun`.\nWe have `ocamlrun` running on the Sail model, compiling programs with the\nreal `boot/ocamlc`. The plan there ends in a fixpoint: if the source\nsemantics says the compiler compiles its own sources to exactly the bytes\nof `boot/ocamlc`, and the compiler’s back end is proved correct, then\nthose bytes get a meaning without verifying their 412,000 bytecode\ninstructions one at a time.\n\nFor both projects, we have already stated the headline theorems in\nLean. What remains is to close their proofs.\n\nThe north star is CPython. We believe that current agents make an\nLLM-written, machine-validated semantics for Python feasible, given\nenough compute. Tools like the ones in the previous section could then\nbe built on it, with guarantees that reach the CPython binary.\n\n---\n\n1. The project was genuinely stuck before iris-lean came out. We\n owe its authors a drink. [↩︎](#fnref:1)\n2. A stronger statement, that the binary reaches a `Loaded`\n state for every well-formed program, would require verifying the\n parser, which runs before `interp_run` and is outside our theorem. [↩︎](#fnref:2)\n","body_html":"

We had LLMs write precise mathematical rules, or a formal semantics, for how a small programming language should behave. We then used Lean, a tool for checking mathematical proofs, to prove that the interpreter—the program that runs code written in that language—follows those rules even after being compiled into low-level instructions understood by a RISC-V computer chip.

\n
\"\"
\n

LLMs are growing alarmingly capable at finding and exploiting bugs in\nproduction software, with increasing reports of AI-assisted hacks\nin the wild.\nFortunately, LLMs are advancing quickly in their ability to write\nverified software: programs that come with mathematical proofs,\nchecked by a computer, that rule out entire classes of bugs.\nIn April, our agents built a JavaScript-to-WebAssembly\ncompiler but could not prove that it preserved\nprogram behaviour. Months later, our agents verified Linux’s nftables\ncompiler, which translates firewall rules\ninto instructions the kernel executes. In September, MIT researchers\nFrans Kaashoek and Nickolai Zeldovich used AI agents to verify the xv6\noperating-system kernel down to its\nmachine code.

\n

Our goal at Basis is to develop verification methods that could plausibly scale to all software, so that the systems powering critical infrastructure are secure by design and keep pace with attackers’ growing capabilities.\nAs LLMs advance in capability, the bottleneck is shifting away from theorem proving and towards the problem of specification: how can we be sure that the statements we prove capture the behaviour we actually care about?

\n

To prove anything about a program, we first need a mathematical description of what it does.\nThis starts with describing the programming language it is written in: what every statement, loop, and function call means when it runs.\nThese descriptions are called a formal semantics, and can be written with pen and paper, but are increasingly expressed in a proof assistant such as Lean.\nA handful of languages have one (Standard ML, WebAssembly, and C via CompCert), as does the RISC-V instruction set that a growing number of processors execute.\nDeveloping each of these semantics took years of expert effort.

\n

Most programs, however, are written in languages that do not have a formal semantics, presenting a major bottleneck for deploying verified software at scale: without a semantics, there is nothing precise to prove against.\nA natural solution is to use LLMs to write semantics, but LLMs make mistakes, and a broken semantics undermines every proof built on it.\nTesting helps, but as we show below, a semantics can pass every test and still be wrong. What is needed is a means to verify the semantics itself.

\n

Languages without a formal semantics still have interpreters or compilers, which in practice define what their programs mean.\nHere we consider a radical idea: make the LLM prove that its semantics agrees with the real interpreter on every program, treating the interpreter as ground truth. To do this, we compile the interpreter to RISC-V, whose meaning is already formally defined. That gives an exact, if unreadable, description of what the interpreter does with any program. The LLM then writes readable rules for the language and proves in Lean that, for every possible program, those rules predict exactly what the compiled interpreter prints. If a rule is wrong, the proof gets stuck.

\n

We report on an experiment where we had LLMs develop a semantics and\nits proof together for a small language. We used Lean to prove that the interpreter, the\nprogram that runs code written in that language, follows those rules\neven after being compiled into low-level machine instructions. The\nwhole development, semantics and proof, is\non GitHub.\nThe rest of this post walks through this\nexperiment, explaining first why semantics are the bottleneck for\nlarger verification efforts and why tests aren’t sufficient to build\ntrust in them. We then show how the proof process refined the semantics,\nhow we handled the memory reasoning, and what tools we built on the result.

\n

Every verified program starts from a semantics

\n

Before you can prove a program does anything, you have to define how\neach operation transforms its state, that is, define its semantics.\nMost languages describe their semantics informally in prose, in a\nreference manual, and leave the concrete details to the compiler or\ninterpreter implementation. A formal\nsemantics writes the rules down in mathematics, precisely enough for a\nproof checker like Lean 4 to use them. Notable examples include\nCompCert’s semantics for C, CakeML’s for ML, and JSCert’s for JavaScript.\nEach one took years of expert effort, and often covers only a restricted\nsubset of its language.

\n

For this experiment we used an extended version of WHILE, the small\nimperative language used in textbooks such as Nielson and Nielson’s\nSemantics with Applications.\nOur version has integers, strings, first-class functions with closures, if, while\nand for loops, and runtime errors. Its interpreter is 1,855 lines of\nC, and a WHILE program looks like this (it prints 55):

\n
var i = 0;\nvar sum = 0;\nwhile (i < 10) {\n    i = i + 1;\n    sum = sum + i;\n}\nprintln(sum);
\n

The semantics an LLM wrote for WHILE is a set of rules, one for each\nkind of expression and statement. These rules describe how to evaluate\nan expression in terms of its subexpressions. For integer addition,\nthe rule is:

\n
st, env ⊢ l ⇓ a, st'    st', env ⊢ r ⇓ b, st''    a + b = c\n──────────────────────────────────────────────────────────\n                 st, env ⊢ l + r ⇓ c, st''
\n

A rule reads from the bottom up. The line at the bottom is its\nconclusion. Starting from state st in environment env, the\nexpression l + r evaluates (⇓) to c and leaves state st''.\nThe state holds variable values, closures and everything printed so\nfar; the environment says which variables are in scope. The premises\nabove the line explain how the result follows from the subexpressions.\nFirst l evaluates to a, leaving state st'. Then r evaluates to\nb in that state, leaving st''. The final premise, a + b = c,\nadds the two integer values using WHILE’s 64-bit wrapping arithmetic.

\n

Take (1 + 1) + x, with state [x ↦ 5] and environment {x}:\nx holds 5 and is in scope. Applying the rule gives:

\n
[x ↦ 5], {x} ⊢ (1 + 1) ⇓ 2, [x ↦ 5]    [x ↦ 5], {x} ⊢ x ⇓ 5, [x ↦ 5]\n                              2 + 5 = 7\n─────────────────────────────────────────────────────────────────────\n              [x ↦ 5], {x} ⊢ (1 + 1) + x ⇓ 7, [x ↦ 5]
\n

That is, to evaluate (1 + 1) + x, we first evaluate (1 + 1) to get\n2, then look up x to get 5, and add the two values to get 7. Neither\nsubexpression changes the state, so [x ↦ 5] remains unchanged.

\n

To justify the first premise, we apply the addition rule again:

\n
[x ↦ 5], {x} ⊢ 1 ⇓ 1, [x ↦ 5]    [x ↦ 5], {x} ⊢ 1 ⇓ 1, [x ↦ 5]\n                           1 + 1 = 2\n───────────────────────────────────────────────────────────────\n              [x ↦ 5], {x} ⊢ 1 + 1 ⇓ 2, [x ↦ 5]
\n

These rule applications form a tree that derives the value of the\nwhole expression from the values of its parts.

\n

The LLM wrote about 400 lines of rules like these, in Lean (the full\nsemantics).\nEach rule looks reasonable on its own, but an end user has no rigorous\nway to tell whether they faithfully describe how WHILE programs behave\nwhen they are actually run.

\n

A semantics can pass every test and still be wrong

\n

The usual way to check a semantics is to run it. Take a test suite,\nrun each program under the semantics and under the real interpreter,\nand compare what they print. Unfortunately, in practice, this process\nis insufficient to build trust in the generated semantics.

\n

For example, an early version of our semantics passed the test suite\ngenerated for the WHILE interpreter, but disagreed with the binary\nwhen a function’s name reached 59 characters:

\n
fn aaa…aaa() {}           // a name of 59 a's\nprintln("" + aaa…aaa);\n\nsemantics:  <fn aaa…aaa>\nbinary:     <fn aaa…aaa
\n

The semantics said that concatenating a function with a string would\ninclude its full name between <fn and >. The binary dropped the\nclosing >, and for longer names it dropped part of the name too.\nNo test in the suite tried functions with names this long.

\n

The reason is in the C\ninterpreter\nthat turns a value into a string when you concatenate it with +:

\n
static char *stringify(Value v) {\n    ...\n    char buf[64];\n    switch (v.kind) {\n    ...\n    case VAL_FN: {\n        const char *name = v.as.fn->fn_expr->as.fn.name;\n        if (name)\n            snprintf(buf, sizeof buf, "<fn %s>", name);\n        else strcpy(buf, "<fn>");\n        break;\n    }\n    default: strcpy(buf, "<native fn>"); break;\n    }\n    ...\n}
\n

stringify returns a string value as it is. Any other value is first\nprinted into a 64-byte buffer on the stack and then copied into a\nfreshly allocated string. A named closure is printed with snprintf as\n<fn name>, an anonymous one as <fn>, and the built-ins fall through\nto the default case, <native fn>.

\n

snprintf writes at most 63 characters into the 64-byte buffer. The\ninitial semantics used the same rendering rule for concatenation and\nprinting, and missed this limit. To prove agreement with the binary,\nthe LLM had to give concatenation its own renderer. The\ncorrected\nsemantics\ncuts a closure’s rendering to its first 63 bytes:

\n
"" + f        ⇓  take 63 ("<fn " ++ f ++ ">")
\n

This is the kind of detail an\nimplementation accumulates internally but nobody writes down\nexplicitly, which is precisely why a semantics transcribed by hand, or\nwritten by an LLM, can miss it. Nor is it a detail no program would\nnotice: code in dynamic languages routinely relies on the string form\nof a function, for logging, for dispatch keyed on a name, or for\ncomparing serialised values. Even simple violations like\nthis undermine any verification effort built\non top of the semantics, and can leave holes that hide security\nvulnerabilities. To build secure and scalable semantics, we need to go\nbeyond tests, since a test suite only checks the programs someone (or\nan agent) thought to write.

\n

Ship your interpreter

\n

Shipping your interpreter means checking the semantics against the\nimplementation people actually run. Compile the interpreter the\nlanguage already has, and make the LLM prove that the binary\nrefines the semantics, that is, that the two agree on what every\nprogram prints.

\n

The theorem we\nproved\nis this one:

\n
theorem endToEnd_refinement :\n  ∀ p c, Loaded interpRunLayout p (fillZero c) →\n    (∀ out, BigStep p out ↔ Halts c out 0) ∧\n    (Diverges c → ¬ ∃ out, BigStep p out)
\n

The theorem says for any WHILE program p, and any machine\nconfiguration c, if the machine configuration satisfies a property\nLoaded, then the semantics match what the compiled binary will\ndo. Loaded interpRunLayout p (fillZero c) here says that c is a\nmachine about to run p through the interpreter binary. The first\nconclusion, (∀ out, BigStep p out ↔ Halts c out 0), says that the\nsemantics derives output out if and only if the machine halts with\nexit code 0 having printed out, i.e. for successfully terminating\nprograms the predicted outputs are equivalent. The second says that any program\np on which the machine runs forever (Diverges c), is a program the\nsemantics derives no terminating output for.

\n

We can visualise this theorem as a commuting square, showing how the\nsemantics and the binary agree on a program’s output. In the diagram\nbelow, the top arrow relates a program p to the output\nout predicted by the semantics. The bottom arrow relates a machine\nstate c to the output printed when the binary halts successfully.\nThe dashed line on the left is the Loaded condition connecting the\nprogram to that machine state. Under this condition, the theorem says\nthe two outputs agree, shown by the double line on the right. The\norange arrow shows how a failed attempt to prove that agreement sends\nthe LLM back to revise a rule of the semantics.

\n
\"The
\n

For a program loaded into the machine, the semantics and successful execution agree on the output.

\n

The theorem catches a wrong semantics in both directions. If the\nsemantics is too permissive, it derives an output the binary never\nprints, and the left-to-right half fails. If it is too strict, it has\nno rule for something the binary does, and the right-to-left half\nfails. Either way the LLM gets a proof obligation it cannot discharge.\nIn our experience, that obligation usually points at the rule that is\nwrong.

\n

RISC-V is an open processor design. We use its formal model, written\nin Sail and translated into Lean,\nto define how each machine instruction executes. The binary is the\nactual ELF executable: 1,855\nlines of interpreter C compiled by gcc, linked against dlmalloc and\nnewlib, 25,336 instructions in all. For comparison, the xv6 kernel\nverified with MachCSL is 8,697 RISC-V instructions, built from 6,593\nlines of C and assembly, although its proof also covers concurrency,\nwhich ours does not need. The C compiler’s output, the C library and\nthe memory allocator are all inside our theorem. A person\nwho wants to trust the result reads the statement above, the hypothesis\nLoaded, and the two short definitions of Halts and Diverges. They\ndo not need to trust BigStep, because the proof checks it against the\nbinary.

\n

Developing the semantics and proof together

\n

Developing the proof forced the LLMs to account for four details in\nthe semantics:

\n

  • integer arithmetic had to wrap at 64 bits, because negating the

    smallest integer was unsatisfiable against the machine;

  • a for loop’s initialiser had to ignore an abrupt status, because

    the C does;

  • built-ins had to render differently in print and in concatenation;
  • long closure names had to be cut at 63 bytes.
\n

Each correction started either as an obligation that would not close\nor as a run of the binary that disagreed with the semantics.

\n

The 63-byte cut is a representative example. The proof of the\nconcatenation case needed the semantics’ rendering to equal the\nbinary’s, and for long names it didn’t, so the obligation could not be\ndischarged until the rule changed.

\n

The proof also caught mistakes in the LLM-generated lemmas about the C\nlibrary. The LLMs stated what each function does and then proved\nthat statement against the machine code. An allocator reserve that no\nheap satisfied after a single malloc(24), a realloc lemma that was\nfalse for sizes that wrap, and an exit routine that writes errno\nwithout its lemma saying so all showed up the same way, as obligations\nthat would not close.

\n

Separation logic makes the binary proof tractable

\n

LLMs wrote all of the proof. Most of the difficulty lay in reasoning\nabout memory. We needed a specification for malloc, the function\nthat allocates memory, which would let us prove that allocating a new\nblock preserves the data already held by the interpreter. Even\nprintln("n = " + x) allocates three strings and frees two of them.\nThroughout those calls, the program’s variables and the half-built\nresult must remain intact.

\n

The textbook way to do this is to give each function a Hoare triple\ntogether with a footprint, a set of bytes the function may write.\nFacts about memory outside the footprint carry across a call\nunchanged. A triple { P } code { Q } reads as “if P holds before\ncode runs, then Q holds after it”. For malloc, such a\nspecification reads roughly as follows, where F is a fixed set of\naddresses:

\n
{ heap H }\n  p := malloc(n)\n{ heap ((p, n) :: H)  and  p is fresh }\nmodifies F
\n

Unfortunately, no such F exists. From the same heap, malloc(32)\nwrites the header of the new top chunk at address 0x82000238, so F\nmust contain that address. malloc(64) instead returns the block\n[0x82000210, 0x82000250), which contains it. Once the caller owns\nthat block, facts about its bytes have to survive later calls, so F\nmust also exclude 0x82000238. The LLMs proved in\nLean\nthat no fixed set of addresses can satisfy both requirements, after a\nfirst attempt that worked around the problem one fact at a\ntime had stalled for three weeks.

\n
\"Two
\n

From the same heap, malloc(32) writes a byte that malloc(64) would hand to the caller. The allocator's write footprint must change as ownership of memory changes.

\n

Separation logic solves this by making the footprint depend on the\nheap. We ported MachCSL, the logic\nbehind the xv6 proof, to the newly released\niris-lean.1 In separation\nlogic the allocator owns the free bytes of its arena, and malloc’s\nspecification\nhands part of them to the caller:

\n
{ isHeap H }\n  p := malloc(n)\n{ (p = 0 ∗ isHeap H)\n  ∨ (isHeap ((p, n) :: H) ∗ blockOwn p n) }
\n

Here ∗ is the separating conjunction, which says that its two\nhalves hold of disjoint parts of memory, and the result p is either\nnull or a fresh block. isHeap H owns every byte of the arena outside\nthe live blocks H. Initially, the allocator owns 0x82000238, so\nmalloc(32) may write it. If the caller instead requests malloc(64),\nthat byte passes to the caller through blockOwn, and later calls\ncannot touch it. Anything else the caller owns is not\nmentioned in the specification, and the frame rule carries it across\nthe call in one step. After the port, the rest of the proof closed in a\nfew days.

\n
\"The
\n

LLMs write the semantics and the proof linking it to the existing interpreter binary; Lean checks that proof against the machine model.

\n

At its peak the proof was about a million lines of Lean, two thirds of\nit generated by 35 scripts the LLMs wrote, which read the binary and\nemit a proof rule for each of about 11,800 instructions. A later pass\nreplaced the generated proof families with abstractions proved once,\nsuch as a symbolic executor for machine code, and brought the proof\nunder 200,000 lines. It uses no axioms beyond Lean’s standard\nones (propext, Classical.choice and Quot.sound).

\n

The theorem applies to real programs

\n

A theorem with a hypothesis is only useful if that hypothesis can be\nsatisfied. If Loaded described a machine state that never occurs,\nour theorem would hold vacuously and tell us nothing about the binary.

\n

We had the LLMs prove in Lean that Loaded holds for ten\nprograms.\nFor each one, they constructed a machine state at the interpreter’s\nentry, with the program in memory alongside the binary, the runtime\nand the allocator. Lean checked that each state met the theorem’s\nprecondition.2

\n
\"A
\n

Loaded specifies the memory and registers needed to run the program through the interpreter binary. The program enters as a syntax tree (orange); the surrounding code and runtime state come from the interpreter.

\n

We also replayed 85,483 machine steps from the executable and checked\nthat the resulting memory matched the constructed state byte for\nbyte. The link from the executable file and its boot trace to that\nstate was checked by scripts; Lean checked the precondition and the\nexecution from that state onwards. For the full loop test\nprogram,\nwhich extends the earlier example with two more sums, the binary\nprovably halts after printing 55, 2500 and 36 on separate lines.

\n

The precondition includes enough heap and stack space for the program.\nA later\ntheorem\nreplaces these two assumptions with checkers that run on the program.

\n

Once you trust the semantics, the tools are cheap

\n

A validated semantics also works as an interface. Anything you prove\nsound against BigStep is sound for the binary, by composing it with\nthe refinement theorem, and that composition is a few lines of\nLean. So we had LLMs build four tools on top of it.

\n
\"A
\n

The type system, program logic and analyser reuse the interpreter's refinement proof. The compiler is proved to implement the same semantics directly on RISC-V.

\n

The refinement proof took about a month and is about 140,000 lines of\nLean. The four tools below were opened as pull requests over three\ndays, and come to about 33,000 lines between them, most of it the\ncompiler.

\n

The first tool is a type\nchecker.\nIt catches invalid operations before a program runs. For example,\nthese two programs are rejected:

\n
"a" - 1;               // subtracting an integer from a string
\n
var x = 1;\nx = "s";               // assigning a string to an integer variable
\n

The proofs for these\nexamples\nshow that neither program can pass the checker. Its soundness theorem\nrules out type errors in accepted programs, including when they run\nthrough the interpreter binary. Division by zero, a failed assert\nand the interpreter’s call-depth limit remain possible; those require\nreasoning about values as well as types.

\n

The second tool is a program\nlogic,\nwhich lets us prove what a particular program computes. The loop near\nthe start of this post adds the integers from 1 to 10. The full test\nprogram\nalso adds the odd integers from 1 to 100, using break and continue,\nand computes a third sum with nested loops. The LLMs used the logic\nto prove that running this program through the interpreter binary\nterminates and prints exactly:

\n
55\n2500\n36
\n

The third tool is an abstract\ninterpreter,\nan analysis that tracks possible values through a program and raises\nalarms for potential runtime errors. It analyses that same test\nprogram with no\nalarms,\nproving it free of runtime errors. It also establishes that the final\nvalues of sum, total and acc are 55, 2500 and 36. The analysis\ncomputes these results automatically, and its soundness proof connects\nthem to execution of the binary.

\n

The fourth tool does without the interpreter entirely. In April, our\nagents built a compiler but could not prove it correct. Here the\nsemantics came first, and the LLMs built a verified\ncompiler\nfrom all of WHILE (strings, closures, calls, for, return and\nassert) straight to RISC-V. Compile the sum program above, and the\nresulting machine code prints the same three numbers. The correctness\ntheorem establishes agreement for every program meeting its\npreconditions. A checked\nversion\nanalyses allocation cost, so its theorem needs no assumption about\navailable heap space.

\n

Dropping the interpreter also makes WHILE programs faster. We ran\nevery program in the interpreter’s test suite both ways on the\nspike RISC-V\nsimulator. Counting the interpreter from the moment it starts evaluating, so that\nparsing is not charged against it, compiled code retires between 2.7\nand 8.2 times fewer instructions, and both routes print the same\noutput. These are instruction counts on a simulator rather than timings\non hardware.

\n
\"Paired
\n

Compiling these WHILE programs reduces instruction counts by a factor of 2.7–8.2 while preserving their output. Counts come from the spike RISC-V simulator and exclude parsing by the interpreter.

\n

Once the semantics is trusted, it is the language, and the binary we\nstarted from is no longer needed to run WHILE programs.

\n

What’s next: Lua, OCaml and, one day, CPython

\n

Our experiment with WHILE targeted a toy language. LLMs developed its\nformal semantics, proved that the compiled interpreter follows it,\nand built verified tools on top. We are now scaling this approach up\nto real languages.

\n

Ship your Lua\ntargets Lua 5.4.7 compiled to bare-metal RISC-V. The binary already\nruns on the Sail model and agrees with native Lua, and the plan cuts\nthe proof at the VM: first the bytecode interpreter against a bytecode\nsemantics, fragment by fragment over opcodes, then the source language\nagainst the bytecode.

\n

Ship your OCaml\ntakes advantage of the way OCaml bootstraps itself. OCaml’s bootstrap compiler is checked\ninto its repository as bytecode, boot/ocamlc, and runs on ocamlrun.\nWe have ocamlrun running on the Sail model, compiling programs with the\nreal boot/ocamlc. The plan there ends in a fixpoint: if the source\nsemantics says the compiler compiles its own sources to exactly the bytes\nof boot/ocamlc, and the compiler’s back end is proved correct, then\nthose bytes get a meaning without verifying their 412,000 bytecode\ninstructions one at a time.

\n

For both projects, we have already stated the headline theorems in\nLean. What remains is to close their proofs.

\n

The north star is CPython. We believe that current agents make an\nLLM-written, machine-validated semantics for Python feasible, given\nenough compute. Tools like the ones in the previous section could then\nbe built on it, with guarantees that reach the CPython binary.

\n
\n

  1. The project was genuinely stuck before iris-lean came out. We

    owe its authors a drink. ↩︎

  2. A stronger statement, that the binary reaches a Loaded

    state for every well-formed program, would require verifying the\n parser, which runs before interp_run and is outside our theorem. ↩︎

","headings":[{"level":1,"text":"Every verified program starts from a semantics","id":"every-verified-program-starts-from-a-semantics"},{"level":1,"text":"A semantics can pass every test and still be wrong","id":"a-semantics-can-pass-every-test-and-still-be-wrong"},{"level":1,"text":"Ship your interpreter","id":"ship-your-interpreter"},{"level":1,"text":"Developing the semantics and proof together","id":"developing-the-semantics-and-proof-together"},{"level":1,"text":"Separation logic makes the binary proof tractable","id":"separation-logic-makes-the-binary-proof-tractable"},{"level":1,"text":"The theorem applies to real programs","id":"the-theorem-applies-to-real-programs"},{"level":1,"text":"Once you trust the semantics, the tools are cheap","id":"once-you-trust-the-semantics-the-tools-are-cheap"},{"level":1,"text":"What’s next: Lua, OCaml and, one day, CPython","id":"what-s-next-lua-ocaml-and-one-day-cpython"}]}}