From LaTeX and OCaml to LEAN4 and Executables: Lean-Checked Theorems and Generating Proof-Carrying Rust

In the world of software, there is a constant tension between how we write code and how we know it is safe. Programmers use high-level languages to describe complex logic in a way that is readable and manageable, but the machines that run this code speak a much simpler, more rigid language. To get from one to the other, compilers act as translators, but this translation process is where errors often hide. A mistake in the translation can turn a safe instruction into a dangerous one, causing a program to crash or behave unpredictably. For decades, the most reliable way to ensure safety has been to verify the final machine code, but this is difficult because the high-level meaning of the original program is often lost in the process. The question researchers are asking is whether we can keep the clarity of the original high-level language while still proving, with absolute certainty, that the final machine instructions will do exactly what we intend.

Brent Hartshorn has built a system that answers this question by treating a single piece of code as two different things at once. Imagine a document that can be read simultaneously as a mathematical proof and as a set of instructions for a machine. In this new work, the author takes a subset of a programming language called OCaml, which is known for its strict rules about how data is handled, and gives every definition two distinct meanings. First, the code is read as a logical argument, where the structure of the program itself serves as a proof that certain conditions will always be met. Second, the same code is translated into a different language called Rust, which is designed for speed and safety, and then compiled into a program that a computer can actually run. The brilliance of the approach lies in the verification: the logical proof is checked by a small, trusted mathematical engine, while the running program is checked against a reference interpreter that simulates the code step-by-step. If the two match, and if the logical proof holds up, the result is a piece of software that comes with its own certificate of safety.

The researchers started by building a translator that understands a specific slice of OCaml. This translator, written in Python, is small enough to be read and understood by a single person, which is crucial because if the translator itself is too complex, we cannot trust its output. It takes the OCaml code and splits it into two paths. On the proof path, it converts the code into a format that a mathematical kernel can check. This kernel is a tiny program that acts as a judge, verifying that the logic is sound without making any assumptions. On the program path, the translator converts the code into Rust, a language that is compiled into fast, native machine code. To ensure the translation was perfect, the team also built a reference interpreter that runs the original OCaml code directly. They then ran thirteen different example programs through both the compiled Rust version and the interpreter. In every single case, the compiled code produced the exact same output as the interpreter, proving that the translation process did not alter the behavior of the programs.

Once the code was successfully translated, the team applied a rigorous safety check to the compiled Rust version. They treated the compiled code as a contract, where specific rules about how the program should behave were written down as mathematical theorems. For instance, they checked that integer calculations would never accidentally overflow and wrap around to a negative number, a common source of bugs in software. They found that while most of these safety rules held true, there were specific edge cases where the rules were broken. In eleven different scenarios, the compiled code reached a point where an integer calculation could wrap around, such as when subtracting the smallest possible number from zero. The system correctly identified these as open obligations, meaning the code was safe everywhere except for these specific, known limits. Out of ninety total safety checks performed on the example programs, seventy-nine were fully proved, while the remaining eleven were left open because they represented real, reachable limits in the way the computer handles numbers.

The project went further by applying this method to a small operating system kernel, a core piece of software that manages computer resources. The researchers took a kernel that had previously been written in Python and Rust and rewrote it in their OCaml subset. They then translated this new version into Rust and compiled it. The result was a third implementation of the same kernel. When tested against the original Python version, the new OCaml-derived version answered correctly in all 236 test cases. The team then attempted to prove the safety of this new kernel. They successfully proved 227 of the 236 safety obligations. The few that remained unproved were not errors in the code, but rather gaps in the mathematical tools used to check them, specifically regarding how the system handles complex loops and counters. This demonstrated that the method could scale from small examples to a functional operating system component.

Perhaps the most striking part of the work was the ability to turn a mathematical equation directly into a working program. The researchers took a formal equation that described the behavior of a kernel, written in a standard mathematical notation, and fed it into a tool that converted it into OCaml code. This code was then compiled and run. The resulting program behaved exactly as the equation described, matching the output of the original Python model in every instance. This process showed that a high-level mathematical description could be transformed into a verified, executable binary without losing its meaning. The team proved that the compiled version of this equation satisfied most of its safety contracts, though some of the more complex logical steps required further refinement in the checking tools.

The findings of this work suggest a new path for building reliable software. By keeping the high-level source code and verifying both its logical meaning and its compiled form, the researchers created a system where the safety of the final program is backed by a mathematical proof. The method successfully identified real-world limitations in how computers handle numbers, such as integer overflow, and distinguished them from actual bugs. While the system did not prove every single safety rule for the most complex parts of the kernel, it proved the vast majority, and the ones that remained open were clearly identified as areas where the checking tools, rather than the code itself, needed improvement. The work stands as a demonstration that it is possible to own the translation process from high-level code to machine instructions, ensuring that the final executable carries a certificate of safety that is as rigorous as the logic that created it.