# Doré Protocol

> Commodity trade finance, formally verified.

## Docs

- [The ceiling](/ceiling): The ceiling answers one question: over the declared design space, what is the
most the protocol can earn while surviving every stress scenario and keeping
every counterparty at the table?
- [Onchain](/cf-defi): This page covers the part of the subject that is genuinely new: what happens
when a commodity facility is represented onchain, which DeFi primitives it
meets there, and — the question that matters most — what tokenization does and
does not transfer.
- [Financing instruments](/cf-instruments): There appear to be dozens of commodity-finance structures. There are really
only a few, distinguished by **what stage of the trade they finance** and
**where repayment comes from**. Learn those two axes and the catalogue
collapses.
- [Who finances what](/cf-market): Commodity finance is populated by institutions that each control one scarce
capability and trade with each other for the rest. This page is the capability
map, then a sourced map of real institutions occupying each layer.
- [Risk, collateral and protection](/cf-risk): Financing a commodity trade means holding a bundle of quite different risks and
then taking them apart. This page is the taxonomy, the security stack that
addresses it, and — importantly — what protection does *not* do.
- [What commodity finance is](/cf): You cannot evaluate Doré without first understanding the industry it operates
in. This section teaches that industry — briefly, but structurally — before any
page describes the protocol. Read these five pages in order and the
[litepaper](/litepaper) will read as a set of engineering choices rather than
assertions.
- [DrUSD — the payment leg](/contracts-drusd): A fiat-referenced token: reserve-backed, redeemable one-for-one at will.
- [FacilityRegistry — the settlement gate](/contracts-facility): Registers facility occurrences and gates their settlement.
- [SdrUSD — the yield leg](/contracts-sdrusd): A pro-rata share of the strategy pool, redeemable through a queue whose length
matches the facility cycle.
- [LiquidationWaterfall](/contracts-waterfall): On a breach of the minimum-value rule or a pooling event, proceeds are
distributed in a fixed order: holders first up to par value, then any further
holder entitlement under the white paper, then general creditors.
- [Contract architecture](/contracts): Four contracts, each implementing rules that were proved before they were
coded. The test suite is the bridge: every test names the theorem or the
sourced provision it discharges.
- [Development](/development): The hygiene gate fails on any `sorry`, `admit`, `native_decide`, custom axiom
or compiler warning. Axiom audits are run on every headline theorem; the
development uses only `propext`, `Classical.choice` and `Quot.sound`, and many
results use none.
- [How Doré makes money](/economics): The business model is one sentence: **Doré originates commodity-finance yield,
passes most of it to token holders, and keeps the spread.** Everything below is
that sentence with numbers on it — the plan as the investor deck states it,
then what our own proofs say about whether the plan closes.
- [ADGM position](/legal): The legal work is done against operative text, fetched and hashed, not against
summaries. Ten documents are in the source registry with SHA-256 hashes and
recorded effective dates.
- [Litepaper](/litepaper): **Financing the metal before it is money.**
- [The commodity pipeline](/pipeline): Most of this documentation describes what Doré proves. This page describes what
Doré is *about*: how a physical commodity actually moves from the ground to a
buyer, who touches it, what paper is created at each step, and where financing
attaches. Everything downstream — the claim schema, the archetypes, the cost
model, the ceiling — is a formalization of the process on this page.
- [Every player](/players): Doré is a two-sided market. It only exists if both sides are onboarded: claim
issuers who need capital, and holders who supply it. A model that maximizes
protocol profit while starving either side is a spreadsheet, not a design.
- [What is proved, and what is not](/proved): 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.
- [Sourced provisions](/provisions): Every rule below was parsed from operative text with a recorded hash. Where a
provision is quoted in the development, it is quoted verbatim with elisions
marked.