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. Each quote is paired with an execution-proof panel that surfaces spec conformance and verification posture next to the trade.
ZenoDEX demonstrates claim boundaries, public replay, negative evidence, and the difference between bounded assurance and a production guarantee.

What a reviewer should inspect first

  1. README.md - public assurance snapshot and assurance shape.
  2. docs/PUBLIC_ASSURANCE_REPLAY.md - clean-checkout replay posture.
  3. docs/claims_registry.yaml - claim status vocabulary.
  4. lean-mathlib/Proofs/ - theorem surfaces.
  5. .github/workflows/ - ratchets, hygiene, and regression gates.

Claim / evidence map

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 surfaces. Lean files around exact-in / exact-out / batch canonicality and uniqueness. Partial / theorem-surface specific
All future DEX behavior is safe. Would require unbounded proof, complete spec, deployment assumptions, and external review. Not claimed

Limitations to state clearly

  • 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