Explanation
Why Lema works the way it does, where its ideas come from, and where the project stands.
These pages give the reasons behind the design: why contracts, implementations and proofs are kept apart, why code is stored by identity, what the kernel does and does not check, and which decisions shaped the current tools. Read them in any order. For the current state of the project, start with Project status and roadmap.
- Build software like mathematics Why Lema separates contracts from implementations and proofs, and what it takes to build on proved results.
- Contracts, implementations and proofs The three roles every checked component plays, how they become store objects, and the three jobs theorems do in an application.
- Code stored by identity Why every object is identified by a hash of its canonical form, and what that does and does not keep stable when code changes.
- How acceptance works What happens between a draft and an accepted object, what the kernel replay checks, and why every native call runs in a sandbox.
- Programs that talk to the world How the Program core describes programs that issue commands, states the protocols they follow, and proves clients and handlers separately.
- Checked, tested and assumed What the three evidence words mean in Lema, why they are kept apart, and what no claim covers.
- Projects, history and review How Lema versions a project's selection of objects and its evidence by identity, and what LemaHub would add.
- How programs reach the outside world Why Lema applications touch the network, files, credentials and clock only through four flat-byte primitives, and what stays assumed.
- Project status and roadmap What works in Lema as of 17 Oct 2026, what is in progress, what was retired, and what comes next.
- Where the ideas come from The languages, systems and papers Lema builds on, what it takes from each, and where it departs from them.
- Design decisions A short summary of each design and working decision that still governs how Lema is built, with its date.