How much does verified mean?

What the checker proves when it accepts a Rust rewrite, what it cannot see, and every problem known so far with the rewrites that passed it. Nothing here is an estimate: the numbers come from the repository's own records.

Loading the numbers.

The short answer

A rewrite is verified when the original function and its Rust version, started from exactly the same state, did the same observable things on at least a thousand generated inputs. Under the current rules a deliberately broken copy of the rewrite must also fail the same test, to show the test can see a change; most rewrites were accepted before that rule existed. A pass is strong evidence about one function in isolation. It is not yet evidence that the rewrites work together inside the running game: that is a second gate, described below, and the problems listed further down are what stands between the two.

  •  rewrites have passed the checker
  •  of them under checker version 2 or later, the only ones that count
  •  compile from the repository alone
  •  files carry a known high-severity issue

How verification works

The checker is a program that decides whether a Rust rewrite of one original function behaves the same as the original. It never reads the rewrite's source and never trusts an agent's opinion: it runs both and compares what they do.

  1. Two runs from the same starting state

    The original function is mapped from the game's executable into a small 32-bit test process and run natively. The rewrite is a function exported from a 32-bit library. For each trial the checker fills memory, the stack and the function's global variables with the same generated contents, runs the original, resets everything to that same state and runs the rewrite. While the rewrite runs, the original's code is made unreadable, so a rewrite that quietly calls the original is caught and reported.

  2. What is compared

    Everything the caller could observe: the return value, every byte written to the heap, the stack and the declared globals, how far the stack pointer moved, every outgoing call with its arguments in order, and whether either side faulted. Floating-point results must match bit for bit, including the sign and payload of a not-a-number. One trial is one set of inputs; a pass needs at least a thousand trials with no difference.

  3. The contract

    Each function has a contract: a small file that tells the checker how to call it (its calling convention and arguments), what inputs to generate (including edge values such as zero, negative numbers and null pointers), which other functions it calls and what those should answer, and which observations to compare. A validator (validate_contracts.py) rejects a malformed contract before it runs, because the checker would otherwise skip a misspelt setting without a word.

  4. The wrong version

    A passing test proves little if the test cannot see a change. So every function also gets a deliberately wrong version: the same rewrite with one change, such as a flipped comparison, a constant off by one or a dropped memory write, run through the same contract. It must fail. If it passes, the contract is blind to what was changed: it is widened, or the function is deferred. When this became a rule, 6,515 of the 6,776 rewrites accepted until then had never had one; a generator (mutate_rewrite.py) now writes many wrong versions per rewrite to map what each contract can see.

  5. The pass is checked for emptiness

    Since checker version 3, a verdict with no differences still fails as vacuous unless at least a tenth of the trials ran to completion on the original without a fault, every enabled comparison actually happened on some trial, and every callee the contract declares was called on some completed trial. A contract may lower these thresholds or exempt a callee, but only in writing, where a reviewer can see it.

What a proof does not cover

Rule 3 of the project asks that anything narrowing a proof is listed in that function's result. A narrowed proof that says so is acceptable; one that looks complete and is not is a defect. These are the usual narrowings, and what each leaves out:

Callees are stubbed
Every call the function makes lands on a recording stub that logs the arguments and returns a scripted answer. The proof says the function behaves the same given those answers; it says nothing about the callee itself, which is proven separately or not yet. Operating-system calls are never run, only recorded.
Full-data checking switched off
Normally a write anywhere in the program's data is seen. A contract can switch that off and compare only the globals it declares; a stray write elsewhere would then go unseen.
Skipped or masked arguments
A call argument can be left out of the comparison or compared through a mask. This is common for a pointer into the caller's own frame, whose address legitimately differs between the two runs; the words it points to are compared instead, through a snapshot taken at the call.
Branches the inputs never take
The inputs are generated. A branch they never reach is not tested, and the emptiness rule can only catch it when the branch would have made a declared call.
The floating-point register stack
Older 32-bit code keeps floating-point values on the x87 register stack. Comparing its final state is a newer check that a contract switches on; the x87 control word, the SSE status register and the floating-point condition codes after return are never compared.
Return value or checks switched off
A contract can compare only the low 8 or 16 bits of the return value, none of it, allow a floating-point tolerance, or switch off a comparison such as the stack or the outgoing calls. Each of these is listed by name by the validator.
Code the checker cannot reach
Functions in the first megabyte of code, which is encrypted in the file on disk, cannot be checked yet. Neither can behaviour that needs a running game (live object graphs, open files), timing, or anything after the first fault in a trial.

The second gate: the game itself

Passing the checker is the first gate. The second is the running game. The verified rewrites are assembled into one library (assemble.py), in shards of a few hundred so no single build is large. A loader that sits beside the game as a stand-in for a system library (lf-proxy) waits until the game is ready, then hooks each replacement with its own switch, all off at the start. A control file turns them on one at a time, a subsystem at a time, or all at once. If the game misbehaves, a bisect command switches on half of the suspects, then half of the half, until the faulty replacement is found. The loader and its switches are tested on a small test program; the phase in progress ends when the game plays with every replacement switched on.

What has passed, and under which checker

Loading.

Passed, by checker version

Version 1 results no longer count as verified; re-run lanes replace them as they pass under a later version.

    Passed, by kind

    Script natives are the engine functions that the game's mission scripts call by name; the rest are ordinary engine functions.

      Written but not passed

      Rewrites that exist in the repository but are not verified. They are never counted as rewritten or verified.

        Why the deferred ones were deferred

        A lane that cannot verify a function gives one reason from a fixed list.

            Known problems with the rewrites that passed

            Every problem anyone has found with a verified rewrite goes into one issue log in the repository, from three sources: pattern checks run over every file, a build check that compiles every file from the repository alone, and reviews in which an agent reads each rewrite against its contract. Every issue stays open until it is fixed or judged not to be one.

            Loading.

            By severity

            High: wrong or unsafe once assembled into the game. Medium: likely to matter. Low: worth tidying.

              By when it matters

              Some issues must be fixed now; most matter once the rewrites run in the game, or when they are turned into portable 64-bit code.

                By kind

                What sort of problem it is.

                  By who found it

                  A file can be flagged by more than one source.

                    Which pattern checks fired, and how often

                      Seven kinds of problem, in plain words

                      These are the classes of problem that matter most for running the rewrites in the game. Each count is of issues whose wording matches the class, so the counts are approximate, and one file can appear in more than one class.

                      • Helper code that only existed in a lane

                        Each agent lane proved its rewrites inside a small crate of its own, sometimes with helper functions written for that crate. Only the rewrite file was kept, so a file that leaned on such a helper no longer compiles from the repository. What was proven can then no longer be rebuilt, and the file cannot go into the library that will run in the game.

                        Being done: the build check lists every file that does not compile against the shared runtime alone; the assembler leaves those files out of the library and records why. One old runtime name that is the shared runtime under another name is mapped to it. Moving the missing helpers into the shared runtime, or re-running the function, brings a file back.

                      • Stack-cookie checks without a cookie

                        Many original functions end with a check the compiler inserted: a secret value, the stack cookie, is placed in the function's frame on entry and compared with the program's copy before returning, so a buffer overrun is caught. In the checker that call is a stub that only records it, so a rewrite that calls it with no cookie, or with zero, still passes. In the game the real check would see a wrong value and end the process.

                        Being done: each is logged to be fixed before the library is switched on in the game, by passing the real cookie or by dropping the call, which a Rust function does not need. Checker version 4 also added a stub that leaves registers untouched, as the real check does, after a stub that overwrote the return value had made correct rewrites fail.

                      • Buffers smaller than the real callee writes

                        Some functions hand a buffer on their own stack to a helper that fills it. In the checker that helper is a stub that writes only the words the contract scripts, so a buffer that is too small still passes. The real helper writes its whole structure and would overwrite whatever lies past the end of the rewrite's buffer.

                        Being done: reviewers compare each buffer with the sizes that sibling rewrites read back from the same helper; the fix is to size the buffer to the structure the original's frame holds.

                      • Float results read from the wrong register

                        On 32-bit Windows a function that returns a floating-point number leaves it on the x87 register stack, while whole numbers come back in a general register. A few rewrites read a callee's floating-point answer from the general register. A checker stub answers wherever the contract tells it to, so the mistake passes; the real callee leaves that register holding something unrelated.

                        Being done: logged per file; the fix is to declare the callee as returning a float, as sibling rewrites do, and to re-run the proof with the callee's answer scripted on the x87 stack, which a contract can express.

                      • Partial proofs

                        A proof is partial when part of the function is not compared: an argument skipped, a callee's answer replaced by a constant, a branch the inputs never reach, part of the code left as a placeholder. Narrowing is allowed when it is stated. It is a problem when a proof looks complete and is not.

                        Being done: pattern checks look for the signs in every file, reviewers read for them, and the contract validator lists every narrowing a contract declares. Proof records, a format added on 4 October 2026, can carry that list with each result.

                      • Misaligned plain reads and writes

                        A plain read through a pointer in Rust promises that the address is aligned, a multiple of the value's size. Game data often is not. The x86 processor tolerates it and the release build the checker uses works, but it is undefined behaviour: a debug build checks alignment and stops, and the optimiser is allowed to assume alignment. Most rewrites use plain reads of game memory; a few use them at offsets that are provably odd.

                        Being done: the odd-offset cases are listed per file; the rest are converted to unaligned reads and writes, which many files already use. Until then the assembled library is built in release, where debug assertions are off.

                      • Overflow that only a debug build notices

                        The original's arithmetic wraps around silently when a number overflows. Rust does the same in a release build, which is how the checker builds every rewrite, but a debug build stops with a panic instead. The same code is then correct or crashes depending on one build setting.

                        Being done: the assembled library is built in release, where overflow checks are off; converting the arithmetic to explicit wrapping removes the dependence on the setting, and reviewers flag the additions most likely to overflow.

                      Found in nearly every file

                      Two patterns are so common that the pattern checks count them once across the whole tree rather than file by file.

                        What is being done, and where to look

                        • The issue log holds every issue above, one entry per file, with its severity, when it matters, who found it and its status. It is regenerated by issue_log.py, which keeps a reviewer's verdict on each issue.
                        • lint_rewrites.py runs the pattern checks over every verified rewrite: what the checker cannot see, and what will matter once the rewrites are assembled.
                        • check_rewrites_build.py compiles every verified rewrite against the shared runtime alone and lists the ones that do not build.
                        • ledger.py checks the rewrite tree against itself and against the published counts, and validates proof records.
                        • mutate_rewrite.py writes wrong versions of a rewrite to find contracts that cannot see a change, and validate_contracts.py lists every narrowing a contract declares.
                        • assemble.py builds the library for the second gate and records which rewrites it left out, and why.

                        Each of these is described, with the command that runs it, on the tools page. The words used on this page are defined in its glossary.