To ensure software is secure by design, researchers often use formal verification—a process of using mathematical proofs to rule out entire classes of bugs. A primary hurdle in this field is the 'specification' problem: to prove a program is correct, one must first define a formal semantics (a precise mathematical description of how every statement and loop behaves). While some languages like WebAssembly or C have established semantics, many others do not. Without a precise specification, there is no ground truth against which to prove a program's safety.

Basis researchers addressed this by using Large Language Models (LLMs) to generate these semantics for a small imperative language called WHILE. However, because LLMs can make mistakes, a flawed semantics would invalidate any subsequent proofs. To solve this, the team proposed a 'radical' approach: treating the existing interpreter—the actual program that runs the code—as the ground truth. They compiled the C-based interpreter into RISC-V machine code, which has a formally defined instruction set. They then tasked an LLM with writing a set of readable rules (the semantics) and a mathematical proof in Lean (a proof assistant) to demonstrate that these rules perfectly predict the behavior of the compiled binary.

A technical diagram showing the relationship between program inputs, machine states, and the iterative correction of semantics.
The research methodology uses a feedback loop where failed proof obligations are returned to the semantics for correction until they align with the compiled binary's behavior.www.basis.ai

The diagram illustrates the 'radical' approach of using the compiled interpreter as the ground truth to debug and refine the high-level semantics.

This method forced the LLM to account for subtle implementation details that are often omitted from human-written specifications. For example, the proof failed initially because the LLM's semantics did not account for a 63-byte limit on how the C interpreter renders function names into strings. The proof only 'closed' once the semantics were corrected to match the binary's actual behavior. By using the compiled interpreter as the anchor, the researchers created a system where the proof process itself acts as a debugger for the semantics. If the proof fails, it indicates a discrepancy between the high-level rules and the low-level execution, forcing the model to refine the rules until they align perfectly with the machine code.

A three-lane development diagram showing fixed inputs, LLM-generated components, and checked outputs.
The development pipeline separates fixed inputs like the RISC-V kernel from the LLM-generated semantics and the resulting refinement theorems.www.basis.ai

This visual explains the structural division of the project between fixed hardware/software anchors and the components generated by the LLM.