Doré Protocol
Commodity trade finance, on-chain — with the economics and the law carried as machine-checked proofs rather than prose.
Doré finances the oldest secured lending there is: short-dated, insured purchase of physical metal that already exists. Two tokens do one job each. drUSD is the payment leg — treasury-backed, redeemable one-for-one at will. sdrUSD is the yield leg — stake drUSD to take a pro-rata share of a pool of insured, asset-secured facilities.
What makes this different
Most protocols document intentions. This one ships a formal development in Lean 4 that the contracts are built to satisfy, and a test suite in which every test names the theorem it discharges.
| Claim | Where it is proved |
|---|---|
| Reserves cover outstanding claims at all times | COBS 19A.7.1, parsed; fractional_backing_fails_min_value |
| A redemption cannot settle before it is due | settlement_never_premature |
| A redemption never pays more than its pro-rata share | FairShareBurn, burn_payout_le_nav |
| A wrong-owner collection cannot be laundered | link_violation_immune_to_reassignment |
| Holders rank first in liquidation, capped at par | COBS 19A.11.4; frt_distribute_holders_first_par_capped |
| No player gains without production | surplus_identity, no_surplus_without_production |
What is not claimed
The formal work is scoped, and the scope is published. No architecture is legally feasible today — the drUSD classification is resolved, the permission is not granted. The economic results are grid optima over a declared model, not continuous claims. Every calibration input is marked sourced or unverified, and the results that depend on unverified inputs are reported as frontiers rather than conclusions.
See What is proved for the honest boundary.