A Lean proof says something about a Lean definition. Running that definition as Rust adds links to the chain between the proof and the running program. This page describes those links, how each is checked, and what the build isolates and what it does not.
What a proof covers
Lean’s kernel checks proofs during lake build, before lungo sees anything. lungo
adds no reasoning of its own: a theorem about Shapes.area holds for the Rust area exactly
insofar as the Rust code computes what the Lean definition computes. The question is
therefore how much one has to trust to believe that it does.
A theorem becomes part of what a package says about itself when it is registered as a claim
about an export (@[lungo_claim]): lungo checks that it is a theorem about that export, and
carries its statement, its status and what it rests on into every generated package. What
claims mean, and how they relate to specifications, assumptions and the trusted base below, is
the subject of formal assurance.
The trusted base
- The Lean toolchain. Its elaborator, kernel and compiler, as
lake buildruns them. Anyone running Lean code natively trusts the same components. - The worker’s adapter. It reads the compiler’s output and metadata and encodes them; it transforms no code. Its assurance pass reads the records lungo’s Lean library writes and checks them again against the environment: that a claim’s evidence is a theorem, that its statement mentions its subjects and specifications and has the shape its relation requires, which axioms the proof depends on. It decides nothing a proof could; it reports what Lean’s kernel accepted.
- The backends. The translation of each Bridge IR instruction into Rust and into C, the Rust facade’s conversions, the language bindings’ encoding of values, and the runtime’s primitives.
- The distribution of the prebuilt runtime, for languages other than Rust (see the runtime distribution).
- The host’s facilities. The operations the application implements (in Rust, Go, Python, Swift, TypeScript or C) are outside every proof. What a claim needs of them it states as an assumption, and the claim holds only on a host that makes the assumption true.
The first is Lean’s responsibility, the last the application’s. The others are lungo’s, and each is checked from a different side.
How the backend is checked
Independent verification of the input. Before generating code, lungo checks the Bridge IR on its own terms: variables and join points in scope, calls with the right number and representation of arguments, literals in range, every called declaration present. A defect in the worker surfaces as a verification error instead of wrong Rust.
Comparison with Lean’s own backend. The conformance programs are compiled three times, as Rust, as C on the runtime’s C library, and by Lean’s native backend, and their output, error output and exit codes must agree byte for byte. The corpus covers every instruction the toolchain emits. Separately, a library of exported functions runs on both backends in one process, compared call by call over generated inputs: large numbers, Unicode text, floats including NaN and negative zero, trees, closures in both directions, IO errors.
Ties to the toolchain. Every extern symbol of the standard library is accounted for with the representation Lean declares, and the complete executable standard library, about fifty thousand compiled declarations, passes verification and generates Rust that type-checks.
One program in every language. A program using every kind of value that crosses the
boundary (big numbers, structures, recursive and polymorphic types, options, arrays, pairs,
Except, closures in both directions, opaque values, IO and EIO errors, host facilities,
async programs answered by a handler, main, concurrent calls) is generated for C, Go, Python,
Swift, Objective-C and TypeScript, and each language’s tests make the same assertions on it,
including on the assurance document each package carries. Each support library, and the
runtime itself, is also checked against shared test vectors of the
wire format, including encodings every codec must reject.
Types shared between packages. A program built on another program’s model reads that program’s values at the layout it was compiled for. Every generated type carries a digest of its layout (its constructors, their fields and every type they reach, with the Lean version), and a package using another package’s type checks it before it runs (see extern types), so two packages generated from different definitions of a type cannot be used together.
None of this is a proof of the backend. It is the level of assurance of a compiler that is tested against a reference implementation, and the reference is Lean’s own.
Trust metadata
Some Lean code is outside what proofs vouch for: definitions that use sorry, axioms beyond
Lean’s standard three, unsafe code, partial definitions, and native externs, among them the
operations of the host’s facilities. lungo computes, for every export, which of these its
executable code depends on, and for every claim which axioms its proof depends on and whether
it uses sorry; it records both in each package’s assurance document, and can refuse to build
when an export or a claim’s proof depends on sorry or extra axioms, or an export on unsafe
code (see how to enforce trust and assurance policies).
A claim whose proof uses sorry is reported as incomplete, never as proved. A proved claim
that rests on an assumption about a facility is reported with that assumption, and every export
it is about lists it: the claim says what holds on a host keeping the assumption, and nothing
about a host that does not. This makes the assumptions behind a function visible where it is
used, in every language.
What the build isolates
Building a Lean project runs its code: macros, elaborators and tactics run during lake build,
and the worker loads the project’s compiled code. Adding a Lean dependency is therefore like
adding a Cargo build dependency or procedural macro: it runs with your permissions.
The worker runs as a separate process under supervision. A crash, a hang or a malformed response is a build error, never a failure of Cargo itself; a timeout kills every process the worker started. Optional limits bound its processor time and memory where the operating system can enforce them, and a hermetic mode withholds your environment variables. These contain failures and runaway builds. They are not a sandbox: file-system and network access are not restricted, and a malicious dependency is not contained.