Dana Edwards
Back to home

Case study

ZenoDEX: Public Assurance Replay

A decentralized exchange whose dangerous bugs are ruled out by construction. Integer-exact math, machine-checked Lean theorems, TLA⁺ models, and replayable certificates make the failure classes behind nine-figure DeFi hacks unreachable.

Summary

ZenoDEX works as a portfolio artifact because its assurance case is layered: functional core, verified kernels, replayable certificate layer, machine-checked proof layer, and public regression layer. Every bounded claim follows the same path from statement to inspectable evidence.

ZenoDEX evidence path: claim, artifact, replay command, assumptions, limitation. Claim bounded, release-backed Artifact Lean proof · certificate Command public replay script Assumptions stated explicitly Limitation scope of the claim
Each bounded claim resolves to an artifact, a public replay command, explicit assumptions, and a stated limitation. Release-backed claims replay from a clean checkout.
ZenoDEX exchange UI: a swap panel beside an execution-proof verification panel.
The ZenoDEX exchange UI, running locally on preview reserves with no live pool. The panel beside each quote shows the available specification and verification checks for the trade.
ZenoDEX demonstrates claim boundaries, public replay, negative evidence, and the difference between bounded assurance and a production guarantee.

Start here

  1. README.md - public assurance snapshot and assurance shape.
  2. docs/PUBLIC_ASSURANCE_REPLAY.md - instructions for replaying from a clean checkout.
  3. docs/claims_registry.yaml - claim status vocabulary.
  4. lean-mathlib/Proofs/ - theorem statements.
  5. .github/workflows/ - ratchets, hygiene, and regression gates.

Claims and evidence

ClaimEvidence to showStatus
Bounded public assurance claims can be replayed from a clean checkout. Public replay document, commands, generated receipts, and gate scripts. Supported / bounded
Canonical winner properties are represented in Lean theorem statements. Lean files around exact-in / exact-out / batch canonicality and uniqueness. Partial / limited to stated theorems
All future DEX behavior is safe. Would require unbounded proof, complete spec, deployment assumptions, and external review. Not claimed

What this does and doesn't establish

  • Release-backed and public-replay claims have bounded scope.
  • Disaster-state witnesses strengthen fail-closed assurance within the tested boundary.
  • Financial/security systems need independent review before any production trust claim.

Open ZenoDEX on GitHub