Litepaper
Commodity finance fails in a specific, diagnosable way: a trade can be profitable, the metal can physically exist, the buyer can be waiting — and capital still does not arrive, because nothing in the chain converts a real transaction into a claim a lender can independently verify.
Doré is that conversion layer. Every load-bearing claim below is machine-checked against a formal kernel or a hashed legal source, and names the theorem or provision that carries it.
| Theorems | 1,499 |
| Lean modules | 78 |
| Archetypes recorded | 101 |
| Executable instances | 29 |
| Contracts | 3 + 1 library |
| Kernel edits | 0 |
1. The gap
The mistake that sinks most commodity-finance ventures is treating the gap as a shortage of money. It is not. Capital is abundant and actively looking for yield backed by something real. The gap is a repeatable reason why economically attractive transactions fail to reach willing capital — and it sits in the institutional filters between commerce and money, not in the supply of either.
The opportunity is the conversion layer between a real transaction and a financeable claim.
A trade must cross four bridges to become fundable, and it dies if any one is missing:
| Bridge | What is broken |
|---|---|
| The asset exists, but is not visible | The lender cannot independently establish title, custody, quantity, quality, or repayment state |
| The risk exists, but is not separable | Credit, price, legal, logistics, fraud and liquidity risk arrive bundled into one opaque exposure |
| The capital exists, but cannot enter | Mandate, regulation, jurisdiction, ticket size or operational cost blocks an otherwise attractive investment |
| The demand exists, but costs too much to serve | Diligence, documents, monitoring and servicing exceed the economics of a smaller facility |
A bank can therefore reject perfectly good economics — small ticket, new borrower, full country limit, heavy compliance burden, collateral control hard to evidence, unfamiliar legal structure. None of those are judgments about the trade. They are judgments about the filter.
That framing is deliberately narrow. There is no authoritative global commodity-finance figure in our sources and we do not quote one. The addressable market is the subset of transactions that can actually be verified, legally structured, priced, monitored and funded through a system.
2. The pipeline
Nine stages and two clocks — set out in full on the commodity pipeline page. The short version: the physical chain and the financial chain are not synchronised, cash leaves before cash returns, and every stage in between creates a document, a risk, and an opportunity for the claim to become unverifiable.
The second clock is the one that kills deals which survive everything else. A transaction may need cash in days, while diligence, investment committees, documentation, subscriptions and settlement take weeks or months. That is where a protocol has a structural advantage over a committee — not because onchain capital is cheaper, since it is often dearer, but because it can arrive on the timescale the trade actually runs on.
3. What Doré is
Doré does not begin with a token. It begins with a claim: a formal object
carrying who owes what, to whom, when it falls due, what evidence discharges it,
and what security stands behind it. Registration is canonical and append-only,
and settlement is gated on the claim's own terms — settlement_never_premature
proves a facility cannot be settled before its due time.
That closes the first two bridges at once. Title, custody, quantity and repayment state stop being narrative and become state a lender reads directly. And because each risk attaches to a named leg of the claim rather than to the trade as a whole, the bundle comes apart.
drUSD is a payment instrument: par redemption, on demand, no queue, and the contract refuses to mint against reserves it does not hold.
sdrUSD is a pro-rata share of the financing book — not a coupon and not a deposit, but a claim on net asset value that absorbs loss ahead of the protocol. Our own earlier model got this wrong, paying holders a fixed rate and quietly turning them into creditors. The contracts implement the share.
Under both sits a liquidation waterfall implementing a rulebook order rather
than a designer's preference, and a monitor whose verdicts are computed from
settlement receipts — so link_verdicts_immune_to_world_events holds and a
violation cannot be laundered by reassigning a beneficiary.
4. Why the method is the moat
Every protocol in this category says it is audited. Doré makes a stronger claim: the properties that matter are proved, in Lean 4, against a kernel that has not been edited once across 101 archetypes and 1,499 theorems. An audit is a skilled human reading code and not finding a problem. A proof is a machine confirming that a class of problem cannot occur.
The system refuses to reason from law it has not read
This is the single most important design decision in the project. Legal rules
carry a source reference with a hash, and eval_unsourced_never_feasible proves
the feasibility engine cannot return a favourable verdict from an unsourced
rule — not a lint warning, a theorem. When the law changes materially,
material_legal_change_stales_compliance_certificate makes the certificate
bound to the old text provably stale.
The consequence is that our regulatory claims are bounded by what we actually fetched. The fiat-referenced token route resolves to feasible-with-conditions on fetched rulebook text. The fund-side route lands honestly on an unresolved fact naming a rulebook we have not sourced, with the closure path already proved. A system that cannot say "I do not know, and here is precisely why" will eventually say something false.
What proof caught that review would not have
An adversarial audit of our own commitment layer found it uninhabited. Every theorem about it was true and every one was vacuous, because no value could satisfy the premises — it proved things about an empty set. No amount of code review finds that; it looks like a correct, well-tested module. It was caught by attacking the formalization itself, then fixed with digests and a proper encoding.
The same discipline killed a balance-sheet free lunch where an architecture allocated 110% of net asset value, and forced a correction when a design credited a first-loss tranche with absorbing losses it had never been priced for.
5. The economics
Doré earns an intermediation spread: roughly 9–12% asset yield against a disclosed alternative of 4.0–4.5%, most of it passed through. The interesting question is not what that spread is today but what it can ever be, so the design space was searched exhaustively and the maximum proved.
On the deck's disclosed coordinates the calm-scenario ceiling is 462 basis
points, inside a band of 357 to 567 (deck_ceiling_band). The design that
attains it is elegant in a precise sense (the_optimum_is_elegant): no player
can be paid more without another being pushed below the option they would
otherwise take.
Seventeen players sit on a transfer ledger whose central property is an identity
(surplus_identity) — payoffs sum to real production margin plus external carry,
minus real destruction and cost. Every internal leg cancels. Nothing is created
by bookkeeping.
The severe corner
Naming an absorption order is not the same as applying it, so the ledger routes credit loss through the waterfall before anyone is paid. In a calm year this changes nothing, because there is no loss to route. At the severe corner the loss is 693 basis points:
Read that as a holder, not as the protocol. The single-agent model had been charging the protocol for losses a correctly specified capital stack puts on holders and sponsors — flattering the protocol's downside while hiding the holder's. A severe year takes a holder's entire coupon and then some. Better published as a theorem than discovered as a complaint.
6. Time beats price, roughly six to one
A commodity borrower does not compare your coupon to a bank's rate. It compares
it to its own return on capital: margin per cycle times turns per year. Two
things follow, both proved: velocity is a price lever
(roc_rises_with_velocity), and capital is never satiated
(capital_pays_for_itself).
Charging what a real gold cycle actually pays — vault, freight, specie cover,
sourcing audit, customs, and a correspondent bank moving money twice a cycle —
produces the sharpest result in the development, and it is negative: at a 1%
margin on a 30-day cycle the completed pipeline does not finance itself
(modest_pipeline_breaks_participation). The rail's five days cost 150 basis
points of gross against 45 of fees, so time beats price roughly six to one.
We publish the frontier rather than a tuned input, and the frontier is now
bracketed by a sourced worked deal that clears with 2.3× cover
(sourced_worked_deal_clears). Three places the comparison is looser than it
looks — a possible double count on the rail delay, a financing-rate basis
mismatch, and a 5-point advance-rate difference — are set out in full on
the unit economics, along with the exact frontiers.
7. Why this is the future
Tokenised real-world assets have spent this cycle solving the wrong bottleneck. Liquidity was never the scarce input; underwriting was. The reason a $2m gold facility cannot get funded is not that no one has $2m — it is that establishing what is true about that facility costs more than the facility earns. Every serious participant pays, repeatedly and manually, for the same handful of facts: who owns it, where it is, what it is worth, what discharges it, and whether the structure is legal where it sits.
That cost is the whole gap, and it is the one cost a formal system genuinely collapses. Once the claim, its evidence schema, its security interest and its legal route are machine-checkable, diligence stops being a per-deal expense and becomes a per-archetype one. This is why the encyclopedia matters more than any single facility: 101 archetypes recorded, 29 executed as live instances against the kernel, and the marginal cost of the next deal in a known shape approaches zero. That, not a token, is what makes small tickets financeable — precisely the bridge that was missing.
The direction of travel looks unambiguous. Capital is getting more mandate-constrained, not less; regulators are converging on rulebooks explicit enough to encode; and the cost of formal methods keeps falling while the cost of a discovered legal defect keeps rising. In that world the durable advantage belongs to whoever can demonstrate the properties of their claims rather than assert them — to the counterparty, to the regulator, and to the person holding the token.
It disciplines our own roadmap too. The widest legal gate the design currently
passes is proved (dore_ceiling_v020), and so is the fact that the owned-venue
route sits outside today's feasible set
(owned_venue_outside_feasible_set_today). We know which door is shut and what
would open it.
8. What is not proved
A document like this is usually where the qualifications get small. Ours are the point, because the discipline that produces them is what we are selling.
| Item | Status |
|---|---|
| Operator margin per cycle, and cycle length | Partly sourced. A hashed teaching example (1.50% / 14 days) brackets both frontiers; no operator has disclosed its own |
| Insurance premium, monitor fee, every player's outside option | Unverified. Not disclosed by any source; carried as declared parameters |
| Default rate, recovery haircut, basis volatility, hedge cost | Unverified. The course names no benchmark, venue or hedging mechanics |
| Market-maker retainer and issuance fee | Unverified. Held at zero rather than invented; the payoff theorem gives the sensitivity |
| Fund-side legal route | Resolved, and closed. provedInfeasible, blocker named: the fund-manager permission (FSMR Schedule 1; FUNDS 1.1.1(a)). The closure path is proved — it opens when the permission is held |
| Documentary-credit legal wrappers | Open. Rest on ICC texts not yet fetched |
| Islamic instruments | Open. Six archetypes recorded; instancing source-gated, since shariah rulings are interpretation |
| Smart contracts | Tested, not audited. 24 passing tests naming their theorems; no third-party audit, nothing deployed to any chain |
None of these is a proof gap. Each is a place where the system refuses to assert something it cannot source — the behaviour we built it to have. The list gets shorter by supplying documents and measurements, not by rewriting proofs.