Design decisions

A short summary of each design and working decision that still governs how Lema is built, with its date.

The project records each consequential choice as a numbered decision in docs/decisions/ in the lema-lang repository. A record says what was decided, why, and which earlier decisions it amends. This page summarises the decisions in force at commit 5a94951 (17 Oct 2026), as AGENTS.md lists them.

Decisions 0004 to 0021 and 0024 governed only their own experiments. HISTORY.md summarises them, and their records are kept at the tag archive/pre-cleanup-2026-10-14.

Many records separate what the project decided from the consequences that agents then worked out. Agents act under the standing delegation of decision 0003, and the records mark those consequences as delegated decisions. A later decision can amend either part.

Decisions in force

0001 Delivery tracking and OpenSpec

10 Oct 2026. Priorities, status and decisions live in the project’s issue tracker. OpenSpec change specifications are used only for bounded behaviour changes with observable acceptance criteria. An OpenSpec requirement is an engineering specification. It is neither a Lema contract nor proof evidence.

0002 Solo development with AI ownership and review

10 Oct 2026. The project has one human participant. AI agents own implementation, tooling and routine technical review. An agent’s review is never reported as qualified human review.

0003 Standing delegated working model

10 Oct 2026. Agents may make owner decisions on the project’s behalf under a standing delegation. Such choices are recorded as delegated decisions, not as the owner’s personal approval.

0022 Develop first, qualify evidence at meaningful boundaries

12 Oct 2026. Ordinary development goes ahead without a fresh admission or review for each change. That covers editing definitions and proofs, repairing failed proofs and fixing scaffolding. Review and frozen evidence are kept for the places where they protect something: changes to trusted checking code, acceptance of results, and stronger claims. The decision came after a period in which control packages and review rounds had displaced language work. Decision 0033 amends its operating rules.

0023 Sole-human development and agent-reviewed route selection

12 Oct 2026. There is one human on the project, so gates that had required recruited human reviewers use non-author agent review instead. That review does not count as qualified human assurance.

0025 Lean-first core development through the codebase

14 Oct 2026. Lean is the working proof and checking foundation. The project defines and proves a small core in Lean and develops it through canonical codebase objects and the API, with no new production custom checker. Plan v7 became the engineering baseline. The earlier plan’s mandatory pre-build experiment gates had displaced core-language development, so they were superseded and recorded as not passed. Earlier Agda work stays available for reuse, without a second toolchain.

0026 Linux continuation host and non-author agent review

14 Oct 2026. Development moved to a Linux x86_64 host. Code review became resolving the pull-request reviewer’s comments. An extra agent review is optional, for risky changes to trusted code.

0027 What object identity covers

14 Oct 2026. Identity v2 replaced profiles with a namespace object: the Lean version and source githash, the Init base and the encoding version. It also made three other changes:

• the checker’s identity moved into receipts, which stay local to their store;
• the axiom ceiling became store policy, above a fixed floor that no policy can lift;
• objects cite definitions by template and theorems by statement, and each satisfaction’s realizations resolve those citations.

Under v1, moving the checker from one host to another re-addressed 1,655 objects. Proof edits rippled into dependents, and one kernel inductive could have several IDs. Decision 0030 replaced v2’s tree encoding of expressions; the other rules stay in force.

0028 Classical choice in proofs

15 Oct 2026. A new store’s default axiom policy is Lean’s three standard axioms: propext, Quot.sound and Classical.choice. The fixed floor is unchanged. Existing stores keep the policy they were created with, and lema init --axioms propext,Quot.sound still gives the narrower policy. Lean’s UTF-8 theory and many Init lemmas depend on choice, and the alternative was to re-prove them for no gain in what runs. Two checks keep choice out of running code: Lean’s compiler (assumed) and the executable vocabulary check (tested). Acceptance does not.

0029 The Rust backend on hold

16 Oct 2026. The safe-Rust backend, which generated workers from Lean’s IR, is on hold, and applications use Lean’s own compiler. The Rust worker reached about 71% of the Lean-hosted worker’s throughput, later 78.37%, and the corrected worker failed a large-response host test. Lean stays the only proof authority, and the tooling stays Rust. Decision 0033 replaced this decision’s “the code stays” with removal.

0030 Shared expressions and one running encoding

16 Oct 2026. Identity v3 stores each expression as an array of distinct nodes in canonical post-order, with children as indices, instead of as a tree. Maximal sharing is enforced by refusal. One proof had been 2,423 shared nodes but 556,691 tree nodes, and four packages had restructured their proofs to fit the 16 MiB object limit.

The decision also set one running encoding. With no users yet, the old encodings and the migration tool were dropped, and every object ID changed. Committed IDs were regenerated from fresh acceptance, and two sets of objects were re-encoded once by a throwaway converter and then replayed.

0031 Standalone leanc applications under the Flat-Byte FFI rule

16 Oct 2026. New applications are standalone binaries compiled by leanc. In development they run under lean --run with --load-dynlib. Capability primitives pass only flat byte buffers (@& ByteArray → IO ByteArray) or a UInt64, so protocol framing, journaling, recovery and signing stay in Lema, where they can be proved. The shims enforce origins, timeouts, byte bounds and credential redaction, and that is tested. A helper process behind the same Lema signature remains an option for isolating credentials.

The decision also set the Stage 4 gate (full local acceptance on fixtures, with live runs outside it) and limited Stage 5 to store and CLI support plus a static generator. How programs reach the outside world explains the design.

0032 Received structures now, regenerated family helpers after Stage 4

17 Oct 2026. A family received by identity lacks some helpers that the same family compiled from source has, such as structure metadata, ctorIdx and noConfusion. So the same source could elaborate differently when it receives its dependencies. The decoder now registers each received structure’s structure and projection metadata at install, with no change to identity rules or stored objects. Regenerating the missing helpers as stored declarations would re-address objects, so it waits until after the Stage 4 gate.

0033 Change-triggered acceptance, records as evidence, rapid development

17 Oct 2026. With no users yet, superseded code and the suites that guard only it are deleted. Each deletion leaves an archive tag, a HISTORY.md entry and the run records, and formats change without migrations. The decision also sets these rules:

• a native run’s evidence is its records (ledgers, logs, digests, every failure), and its bulk bytes are pruned once it passes;
• the merge gate claims “tested” or “checked locally”, never “accepted”;
• native suites run only when something that could change acceptance has changed;
• host pins are to be recorded rather than enforced;
• the HTTP v1 chain and the M3/M4 apps are retired.

What “checked” means does not change: replay into a store by the pinned Lean 4.34.1 kernel, within the store’s axiom policy above the fixed floor. Much of the decision is not yet carried out at 5a94951. The retired code is still in the tree, and planned runtime changes, such as dropping call budgets and the CPU-pressure refusal, are not in the code yet.