What is proved, and what is not

The Doré formal development is a Lean 4 project of 81 build targets with no sorry, no admit, no custom axioms and no native_decide. Every result below is machine-checked. Every limitation below is recorded in the source itself, not only here.

What "the kernel" means

The word appears on most pages of this site, so it should be pinned down.

The kernel is the small set of modules defining the world state and the transition relation over it: World.lean (actors, assets, security interests, cash), Step.lean (the events and the executable step function that either returns a new world or a specific typed error), and Palm.lean (the domain instance the whole development is checked against). Everything else — the claim layer, the corpus archetypes, the architecture search, the legal engine — is built on that relation and cannot change it.

Two properties follow, and they are the reason the word carries weight here:

It is frozen. The kernel has not been edited across 101 archetypes and roughly 1,500 theorems. When an archetype could not be expressed, the recorded outcome was a limitation, not a kernel change — the project's own records list those limitations by name rather than absorbing them.

Errors are values, not exceptions. A rejected operation returns a named error — .incompatibleSecurity, .quantityMismatch, .premature, .alreadyPerformed — so a negative test asserts which rejection occurred, not merely that something failed. That is why the corpus can prove a double pledge is refused rather than merely untested.

The practical consequence for a reviewer: to trust the archetype results you need to read three modules, not seventy-eight.

Proved

The kernel. Money moves between named parties and is neither created nor destroyed (roster_cash_zero_sum). A facility cannot settle before it is due (settlement_never_premature) — a rule that was recorded but unenforced until an external review rejected the corpus over it. A settlement writes a receipt naming who actually collected, and no later reassignment can rewrite it (link_violation_immune_to_reassignment).

The economics. The seventeen players' payoffs sum to real production margin plus external carry minus real cost — every internal transfer cancels (surplus_identity). With no production and no carry, the players cannot collectively gain (no_surplus_without_production). The protocol's coordinate in that ledger is the objective the ceiling maximizes (protocol_payoff_agrees).

The design. Over the declared class, the participation-feasible optimum is identified, and the constraints that bind at it are named: the borrower's participation sets the price, the holder's sets the pass-through, loss absorption stops the advance. Paying any player above its outside option costs exactly the excess and buys nothing (holder_slack_is_pure_transfer), so tightness is forced rather than assumed.

The law. drUSD satisfies the fiat-referenced-token definition mechanically on sourced text (drusd_meets_frt_definition); sdrUSD satisfies the collective-investment-fund definition (sdrusd_meets_cif_definition). A sub-100% design fails the minimum-value rule outright. Holders rank first in liquidation, capped at par.

Not proved — and why it matters

The legal gate is passed, but not by everything, and not unconditionally. An earlier and much-quoted result here — no_architecture_legally_feasible_today — is still true but is now scoped to the L1 fixture built on unsourced law, where it fails on an unresolved payment-token classification. That classification has since been resolved mechanically on sourced text, and dore_ceiling_v020 proves the adopted baseline passes the widest gate we have built. What remains genuinely open is narrower and sharper: the Accepted-FRT determination has not been sought; the fund-manager permission is not held, so the pooled route is provedInfeasible; and owned-venue designs are proved outside the feasible set today (owned_venue_outside_feasible_set_today). Optimization still cannot launder an open legal question — that part was never the stale half.

The optima are grid optima. The design space is a bounded, enumerated grid. No continuous claim is made anywhere without a separate approximation bound, and none is proved.

The evaluator is a declared one-period model. Seven shock coordinates are read by nothing (eval_arch_ignores_unmodeled_coords). Market closure is an explicit omission. Basis risk is the entire price channel for a hedged design.

Most economic inputs are unverified. Two calibration coordinates are sourced to the deck; nine are not. Every player's outside option is unverified — none is disclosed anywhere. Results depending on them are reported as frontiers, not conclusions. See The physical pipeline for the sharpest example.

No comparison to other protocols exists. Nothing here proves Doré is better than any alternative. No competitor is modeled.