Applying Continuous Formal Methods to Cardano
summary
A concrete report of formal-methods engineering applied to a live Cardano node: a team of 11 formal-methods specialists embeds Agda specs and Haskell prototypes into the CI pipeline, using an Agda-to-Haskell workflow, Plutus/Plutus Core models, QuickCheck/state-machine testing and Agda-generated certificates for untyped optimizer passes now used in production tooling. R&D pushes include Ouroboros Paros (consensus) and Babel fees (cross‑token fee payment). Performance targets drive design—95% within five seconds block diffusion goal—leading to practical limits like 64k–256k acceptable block sizes.
AI-written summary · about
chapters (15)
- 0:00Continuous formal methods at IOG
- 1:27Company background
- 5:26Cardano financial OS
- 8:56Formal methods team
- 13:10Cardano node design
- 16:24Plutus TX formalization
- 19:50CEK machine evaluation
- 21:13Ledger formal specs
- 26:07Consensus type system
- 28:11Networking performance
- 29:57R&D innovation
- 32:47Ouroboros Praos
- 36:38Babel fees model
- 38:22Formal methods challenges
- 43:16Closing remarks
related talks
45mFunctional Smart Contracts
22mCardano: The Blockchain Advantage
45mPresent & Future of Blockchain Ⅱ
45mMarlowe: financial contracts on Blockchain
28mFrom Lambda to Ledger: An Architectural Comparison of Plinth and Plutarch
18mGlobal fintech ecosystem and industry trends
04mrecap
28mHypercycle: Blockchain Layer 2 On Top Of Cardano