Formalising Decentralised Exchanges in Coq
summary
Claims a first formalisation in Coq of a decentralized exchange implementation (Dexter2) capturing cross-contract interactions, proves functional correctness and safety properties and finds inconsistencies between informal spec and reference code. Uses the ConCert framework with trace semantics, QuickChick testing and verified extraction, producing about 1k lines CameLIGO of deployed contract and roughly 5.5k LOC formalisation plus ~3.5k LOC of proofs, and introduces a compositional technique that reduces multi-contract invariants to message-only reasoning.
AI-written summary · about
chapters (9)
- 0:00Decentralized exchanges intro
- 1:03Smart contracts need formal verification
- 2:48ConCert framework
- 4:57How Dexter II works
- 6:41Smart contract interactions
- 9:09Proving contract properties
- 12:00Modular proof composition
- 13:46Verification results
- 14:29Q&A
related talks
04mInterview
16mSpecifying Smart Contract with Hax and ConCert
28mDecentralized Exchanges, the new Financial Market Utilities
56mBlockchain applications in the banking industry
21mFrom High-Level DeFi Properties to Concrete Security Bugs
25mLegal Infrastructure for DeFi and DAOs
29mCompositional Verification of Smart Contracts Through Communication Abstraction
38mThe Duality of Smart Contracts and Electronic Rights