Language projectIn development
Build software
like mathematics.
Lema is an experimental language for software that comes with proofs.
You state what the code must do as a contract. Agents write the implementation and a proof that it meets the contract, and the Lean kernel checks that proof before Lema accepts anything.
Start with the promise.
A contract says what the code must do. For a sort, being in order is not enough: every element has to survive, including the repeated 1.
Standard library · accepted
Std.Canonical.sortBy
- In order
- Each element is at most the next one, for any order that is transitive and total.
- Nothing lost or added
- The result is a permutation of the input: every element keeps its number of copies.
theorem sortBy_sorted {α : Type} (le : α → α → Bool)
(trans : ∀ a b c, le a b = true → le b c = true → le a c = true)
(total : ∀ a b, le a b = true ∨ le b a = true) :
∀ l : List α, (sortBy le l).Pairwise (fun a b => le a b = true)
theorem sortBy_perm {α : Type} (le : α → α → Bool) :
∀ l : List α, (sortBy le l).Perm lInput
[4, 1, 3, 1]Result
[1, 1, 3, 4]Both 1s are kept. This is one input, not a proof; the two theorems cover every list.
Follow the evidence.
Each part has one job and its own identity. Only the kernel decides whether a proof holds.
-
Written by people
Contract
What must be true, small enough to read and review.
-
Written by agents
Implementation
Restricted Lean that computes the result.
-
Written by agents
Proof
An argument that the implementation meets the contract for every input.
-
Checked by the kernel
Kernel replay
The server rebuilds each declaration from its stored form and replays it through the pinned Lean 4.34.1 kernel.
Build on what is known.
Prove a property once, then reuse it by its identity. The standard library already holds accepted proofs for bytes, hashing, signing and request encoding.
Get started.
The repository is private while the language is in development. If you have a checkout, these steps take you to a running server.
-
Set up the machine
The script installs the pinned Rust and Lean, builds
lema, and reports whether this machine can run the sandboxed runtime. It needs Linux on x86_64.Shell scripts/cloud-setup.sh source ~/.lema/env -
Start a store and a server
A store holds accepted objects. The server answers requests for it on a local socket.
$CONFIGis a runtime configuration with an output directory of its own; the second tutorial shows how to write one.Shell lema init --store $STORE lema serve --store $STORE --runtime $CONFIG --socket $SOCK & lema --socket $SOCK info -
Publish a proof
Send restricted Lean to the server. It builds a draft, replays it through the kernel and stores it only if every proof holds.
Publish your first proof
Read the docs.
Four kinds of documentation, each for a different need: learning, doing a task, looking something up, and understanding why.
Tutorials
From a fresh machine to your first accepted proof.
How-to guides
One job at a time, for when you know what you want.
Reference
Commands, methods, formats and definitions.
Explanation
Why Lema works the way it does.