Build software like mathematics

Why Lema separates contracts from implementations and proofs, and what it takes to build on proved results.

Lema is an experimental language. People state what code must do, coding agents write the code and the proofs, and the pinned Lean 4.34.1 kernel checks the proofs. Code lives in a store as objects, each identified by the SHA-256 of its canonical form. Names and source files are views of those objects.

How mathematics builds on proved results

Suppose a mathematician shows that a function is complex differentiable on an open set. They do not then prove, for that function, that it has derivatives of every order, or that it equals its Taylor series near each point. Those results were proved once, for every such function. To use them, you check the hypotheses; you do not re-read the proofs. This is how mathematics accumulates. A theorem’s statement fixes what it says, its proof is found and confirmed once, and anyone whose object meets the hypotheses can use it.

Software is mostly assessed by testing. A test shows that code behaved on the inputs it ran. When a component changes, the code that uses it is tested again, because nothing records which of the component’s properties it relied on. Test results do not build up the way proved results do.

Lema tries to make software accumulate like mathematics. Here is the smallest real case:

/-- An `f` that is the identity pointwise is the identity twice over. -/
theorem twice_id : ∀ (f : Nat → Nat), (∀ x, f x = x) → ∀ x, f (f x) = x :=
  fun f law x => (congrArg f (law x)).trans (law x)

The example has two implementations, implA := fun x => x and implB := fun x => 0 + x. Each comes with a proof that ∀ x, f x = x holds for it. A consumer applies twice_id to either one and gets the result with no new argument about f. In the native run of 16 Oct 2026 (crates/lema-cli/tests/reuse.rs), the kernel replayed twice_id when it was submitted, and every later consumer that used it imported it instead of checking it again. This is one small, measured case, and the reuse tutorial walks through it.

Contracts, implementations and kernel checks

The work is split three ways:

• people write contracts, which are short statements of what must be true;
• agents write the implementations, and the proofs that the implementations meet the contracts;
• the Lean kernel checks every proof against its statement, for every input the statement covers.

The split follows from where the cost now sits. Agents make code cheap to write, but reading thousands of lines of generated code and tests is as slow as ever. A contract is small enough to read. For the properties a contract states, nobody has to read the implementation or the proof, because the kernel has checked that the proof proves exactly that statement.

Today contracts are written in restricted Lean, like implementations and proofs. The server’s view method renders stored statements and definitions in a small contract syntax for reading. No method accepts that syntax as input.

The roadmap states two limits that apply to all of this:

• “A contract only guarantees what it states.” Someone still has to check that a contract is complete enough for its use. Being short is not enough.
• “Contracts state behaviour, not cost.” They say nothing about speed, memory use or timing side channels. A replacement that meets the same contract can be much slower, or leak a key through timing.

Dependent types and content addressing

A proved result can only be reused across a changing codebase if two things hold.

The first is a logic in which a general theorem can take evidence as an argument. In a dependent type theory such as Lean’s, a statement is a type and a proof is a value of that type. twice_id is a function: given f and a proof of ∀ x, f x = x, it returns a proof of ∀ x, f (f x) = x. So one proof serves every implementation that comes with the hypothesis.

The second is a way to cite that theorem that does not break when unrelated things change. In a file-based project, a theorem is cited through the file it lives in, so editing a proof in that file changes what everything downstream was built against. In a Lema store, statements, templates and proofs cite a theorem by the ID of its statement and a definition by the ID of its template. Re-proving a theorem leaves the statements, templates and proofs that cite it unchanged. An accepted object is imported by later submissions, not checked again. Code stored by identity explains the rules and their limits. One limit belongs here: a consumer that wants to use the new proof still needs a new binding and one kernel replay.

Proving inside the language

Lema follows one rule for where guarantees live. Do as much as possible inside the language, where the kernel can check it, and keep what has to be trusted small and written down. At the bottom are three things a proof cannot reach:

• the Lean kernel, which decides every check;
• the compiler toolchain for code that runs (leanc, the distribution’s clang and ld.lld, and the Lean runtime);
• the Flat-Byte FFI: four primitives in lean/cap/LemaCap.lean that pass only byte arrays or a UInt64, with lean/cap/glue.c (50 lines) the only code that touches lean.h, and Rust shims behind them that are tested but not proved.

Everything typed above those bytes is Lema code with proofs. That includes HTTP/1.1 request rendering and response framing (lean/cap/Http1.lean), S3 request signing, and the operation record that recovery reads after a crash. The full list of what is assumed is longer. It adds the Rust acceptance path, Linux, glibc and the operator, and the trusted base reference keeps it. Checked, tested and assumed explains how each claim is labelled.

Every item in the trusted base is something a checked claim rests on without proof. A short, explicit list tells a reader exactly what “checked” depends on.

Layered guarantees

Guarantees compose upward. People working near the bottom prove primitives. People building applications cite those theorems and do not reason about the layer below. The standard library already has a chain like this, in which each module receives the modules it builds on by identity:

All four were accepted through the API on 16 Oct 2026 (standard library reference). A program that signs S3 requests cites the theorems of Std.SigV4. It does not re-prove SHA-256 or reason about byte offsets.

Who it is for

Lema is experimental. Objects have one running encoding, formats change without migrations, and there is no production support. It is built first for developers who want to state what their code must do and have that checked. They can read Lean statements, or the smaller contract syntax, and they work with coding agents. Some of them will prove primitives and protocols; others will build applications on what those primitives guarantee.

The roadmap’s long-term goal is “production-ready, multi-core concurrent business web applications compiled to standalone native binaries”. In the roadmap’s words, “It is a goal, not a claim.” Project status and roadmap says what exists today.