System · design, not in any release
LSPE
Every build is a set of judgements about your program. LSPE makes the compiler account for them: it looks for the source of each one, asks you a recorded question when it cannot find one, and writes the exchange into the binary. It does not promise your program is correct. It promises that no exception is silent.
A design, not a download
As of 2026-10-18 LSPE is a design. No release contains it, there is nothing to install, and
this page carries no date for one. The design itself is written down in the repository as
docs/262 — in Chinese, like the other numbered design documents, which is
where this project keeps plans rather than in a public issue tracker.
What follows is what the design is for, and what it refuses to claim. It is not an announcement of a feature you can turn on.
A design is not a promise. Two things are already known to be impossible, and the design writes them down instead of working around them: no compiler can prove a program free of bugs, and no compiler can settle every question it cannot answer. Everything below is shaped by those two facts.
A receipt for every decision
Today a compiler gives you one bit: the program is accepted or rejected. The reasons stay inside the compiler, and the assumptions it made on the way to "accepted" are not written anywhere you can check.
LSPE adds a record. Every time the compiler lets something through that it could not prove, the binary records which decision it was, what evidence it rested on, and — when a person answered a question — who answered. The binary carries a hash of that record; the derivation stays beside it, outside the binary, so the binary does not grow with it.
That is not "no bugs". Whether a program is free of bugs cannot be decided by a compiler; whether every exception was written down can be. The first is undecidable. The second is a property of the process, and it can be checked offline, after the fact, by someone who does not trust the compiler.
The four parts
LSPE is four things working on one space: the sites in a unit where a decision was made, the obligations those sites carry, the evidence for them, and the record of what happened to each. It is not a fifth checker. The checkers stay where they are.
The questioner
The compiler stops being only a judge. Before it accepts a decision, it looks for a source for it, tries to construct a counterexample, and puts it to the second implementation for agreement. If all three fail, it has a hole — and it says so about itself, not about your code.
The questions
A hole becomes a question with options, a default, and the consequence of each answer. Your answer is recorded. A deferral that is not recorded is itself a compile error, so "I know this is suspicious but cannot say why" stops being knowledge that lives only in someone's head.
The police (LSPC)
Before the build, it hands you the bill: which residual risks you are about to accept, one line per family, with what happens if that family does not hold. It does not block by default. You fix what you want and leave the rest, and what you leave is what gets recorded.
The ledger
Everything the other safety components decide — the reclamation ladder, the memory-safety levels, capability domains, ownership — arrives in one ledger. None of those components is replaced or renamed; the ledger is where their verdicts can be read together and cross-checked.
Why the burden of proof moves
The usual compiler stands outside the program and announces a result. LSPE sits inside the transaction: it names its source, prices what it assumes, and hands you a receipt. When it cannot prove something, it may not say "your code is wrong"; it must say "my proof has a hole here". The first is a claim about you, the second is a claim about the compiler, and the two are kept apart on purpose.
That separation has a cost, and the design pays it: the questioner keeps a log of every type substitution and re-proves its obligations after each one. Rust's own record includes a soundness defect of exactly that shape — a check that held before a substitution, and was not run again after it. A compiler that only asks "is there a source?" would not catch that, because the source existed and had expired.
A clerk is not an authority. The standard and each component keep their own semantics. LSPE records decisions and prices them; it does not decide what is true.
What it does not do
It does not find more memory errors
It finds exceptions that have no source, and evidence that has expired. A program with no such exception can still be wrong.
It does not make a program safer
It makes residual risk impossible to accept silently. Those are two different numbers, and the design keeps them apart rather than trading one for the other.
It does not replace the checkers
The reclamation ladder, the memory-safety levels, capability domains and ownership keep their own names, their own owners and their own criteria. LSPE reads their verdicts.
It is not a way to check less
Closing the audit is a recorded choice that you sign, not a switch that removes checks. The checks keep running either way; what changes is whether the result is written down.
The reclamation ladder is described on its own page, and the authority
for every obligation is the standard. The design document is
docs/262 in the repository.