Project status and roadmap
What works in Lema as of 17 Oct 2026, what is in progress, what was retired, and what comes next.
This page describes the repository as of 17 Oct 2026, at lema-lang commit 5a94951. Lema is an experimental language in early development. There are no users yet, so formats change without migrations, and superseded code is deleted (decision 0033). The lema-lang repository is private while the language is in development, and these docs assume you have a checkout.
The evidence words are those of Checked, tested and assumed. Checked means accepted by kernel replay with the pinned Lean 4.34.1 kernel. “Checked locally” means the pinned Lean checked the files outside any store, which is not acceptance. Tested means run and observed. Where the repository’s documents disagree about a status, this page gives the weaker claim.
What works today
| Area | What exists | Evidence |
|---|---|---|
| Program core | Prog, Contract, Safe, Implements, sound and replacement in lean/core/CoreV2.lean (Core v1 in Core.lean) | checked |
| Objects and identity | canonical objects under encoding lema-core-v3, with IDs pinned by crates/lema-core/tests/identity.rs | tested |
| Acceptance | source-free kernel replay, incremental through cached modules, and lema reverify from scratch | checked, under the module cache’s assumption |
| Axiom policy | new stores allow propext, Quot.sound and Classical.choice above a fixed floor (decision 0028) | applied at every acceptance |
| Server and CLI | lema serve over an owner-only Unix socket, and the lema commands | tested; the Rust acceptance path is assumed |
| Aliases | expectations, generations and idempotency keys | tested; the native suites passed with these rules on 16 Oct 2026 |
| Contract view | the view method renders stored laws and definitions | tested: 70 of 70 contracts round-trip through the API; view does not check its own output |
| Bundles | lema.bundle/v1, received as Received.* names | tested, including native suites |
| Standard library | Std.Text, Std.Map, Std.Fixed, Std.Json part 1, Std.Canonical, Std.Bytes, Std.Sha256Spec, Std.Sha256, Std.Hmac and Std.SigV4 in lean/std | checked |
| JSON | an RFC 8259 and I-JSON codec with exact decimals, and a declarative grammar the decoder is proved equivalent to (lean/json) | checked; the JSON check program tested natively on 17 Oct 2026 |
| Execution | execution manifests and lema build, lema run and lema test, with the lean and lean-native backends | tested natively on 16 and 17 Oct 2026; compilers assumed |
| Capability platform | frames, the capability contract, HTTP/1.1 client exchanges, credentials, S3 requests and the operation record in lean/cap; the shims in crates/lema-cap; the runner | seven lean/cap modules checked on 17 Oct 2026, published with their dependencies (30,178 objects); shims and runner tested |
| Minimal reuse | one generic theorem reused by two implementations (lean/examples/reuse) | checked; measured on 16 Oct 2026, with every prediction holding |
In progress
These features exist and are tested without a runtime, over placeholder receipts. The native suites that would run them against the pinned runtime are written but not yet run:
- projects: snapshots, revisions, project references, policies and actors;
- change reports and merges;
- protected references and reviews, whose Lean side (
lean/core/Transport.lean,Protected.lean) is checked locally only; - static inspection pages from
lema site build, tested on a synthetic store.
Other work in progress:
- Releases (
lema.release/v1). The release rules are tested without a runtime. The documents disagree on whether the native release tests have run, so treat that as unconfirmed. - The collector,
collectOne(lean/cap/Collector.lean), which fetches one JSON resource over HTTPS and archives it to S3. Its 274 theorems are checked locally. They include what a run’s trace holds for each outcome: stored valid, archived invalid, storage outcome unknown. Its modules are not accepted yet, and its execution manifest does not build. Std.Sha256Unboxed, an allocation-free SHA-256. It is checked locally and its executables are tested. The documents disagree on its store acceptance, so treat it as not yet accepted.lean/std/Interval.lean, which adds rounding, square root and intervals toStd.Fixed. It awaits its native test.- Fueled programs (
lean/core/Fueled.lean), which are checked locally. Their acceptance test is not yet run. - Parts of decision 0033, which are not in the code at
5a94951: a Rustlema toolchain install, native tests marked#[ignore]with a committed suite map, host pins recorded rather than enforced, and the removal of the CPU-pressure refusal and of call budgets.
Retired or on hold
| Item | Status | Why |
|---|---|---|
| The Python prototype | retired during the Rust rewrite (milestone M0, 14 to 15 Oct 2026), kept at tag archive/python-tool-2026-10-15 | all tooling is Rust; the Python tool was a prototype |
Identity profiles (legacy, framing-v1, core-v1, http-v1, then http-linux-v1) | gone | a namespace object replaced them in identity v2 (decision 0027), and v3 is the one running encoding (decision 0030) |
The HTTP v1 server chain (lean/http), lean/web, the M3/M4 apps (kv, ledger, fanout), the lema-host workers, and the http-build, http-matrix and host commands | retired under decision 0033, with their records archived; still in the tree at 5a94951 | new applications are standalone leanc binaries (decision 0031), and with no users there is no reason to keep superseded code running |
The Rust backend (crates/lema-backend, lema-spike, --backend rust) | on hold under decision 0029; decision 0033 says to remove it, and it is still present | the Rust worker reached about 71%, later 78.37%, of the Lean-hosted worker’s throughput, and the corrected worker failed a large-response host test |
The flagship ledger application, planned as milestone M6, is not scheduled in the current plan.
Roadmap v2
The current plan, since 16 Oct 2026, is Roadmap v2. It is defined by the header of docs/roadmap.md, docs/research/next-steps-split.md §7 and decision 0031. It has five stages in dependency order, with no calendar dates.
| Stage | Scope | Status |
|---|---|---|
| 1 | identity v3, the parked crates excluded from the test gate, minimal reuse | done |
| 2 | the leanc and lean --run runner, Std.Guarantee.IR profiles, bundles, the execution manifest | delivered parts: lema build, run and test, the profiles NoCopySliceCall, NoBigIntPrimitives and NoBoxOrCtorInCycles, bundles, standalone builds, and received structures (decision 0032); regenerated family helpers come after the Stage 4 gate |
| 3 | pure-Lema SHA-256, HMAC and SigV4 | accepted, apart from the unboxed SHA-256 above |
| 4 | the HTTPS-to-S3 collector and releases | gate not met |
| 5 | revisions, the inspector and static LemaHub pages | delivered parts, tested without a runtime |
The Stage 4 gate
docs/research/next-steps-split.md §7 states the gate: “‘Stage 4 done’ is full local acceptance: deterministic local HTTPS (test CA) and S3 (Docker) fixtures plus all fault-injection, restart and quota cases.” Docker is not usable on the build host, so the S3 side is an in-repo Rust fixture (crates/lema-fixtures). A live run against the real API and storage provider is a separate qualification outside the gate. The operator triggers it, and it is capped at 10 requests.
Delivered toward the gate: the lean/cap layers (checked), the collector’s theorems (checked locally), and the local fixtures and the release rules (tested). Not met: the collector’s manifest does not build, nothing has run the collector against the fixtures, and it is not yet known whether the planned storage provider honours If-None-Match: *. Decisions 0032 and 0033 both treat the gate as still ahead. The regenerated family helpers wait for it, and native suites keep running on the operator’s own Linux host until then.
Stage 5 scope
Decision 0031 limited Stage 5 to store and CLI support plus a static HTML, JSON and text generator. A desktop application, a hosted LemaHub and remote receipts are deferred. Projects, history and review describes what is built.
What is not claimed
- The long-term goal is “production-ready, multi-core concurrent business web applications compiled to standalone native binaries”. The roadmap calls it “a goal, not a claim”.
- No proof of the Lean compiler,
rustc, the OS or network delivery. - No public foundation or production assurance, and no human-qualified review.
- No performance or resource claims: contracts state behaviour, not cost.
- No hosted service: LemaHub exists only as the static pages an operator generates from a store.
- No receipts from other machines: a receipt is trusted only in the store that wrote it.
Design decisions has the record behind each of these choices.
Written against lema-lang at commit 5a94951, 17 Oct 2026.