WG211/M24Hammond

IOG has been deploying a variety of (lightweight) formal methods as part of its commitment to high assurance software engineering for the multi-billion dollar Cardano blockchain. Techniques that are used include development in Haskell, use of type families to restrict functionality to specific successive ledger “eras", formal specification in Agda for the ledger and consensus layers, automated conformance testing of the implementation against the specification, property based testing (including new constraint-based checking in QuickCheck to allow the construction of realistic test cases), rigorous timing analysis using the DeltaQ systems design methodology, use and the development of a type-based mechanism to allow automated upgrades synchronised across the whole system (the “Hard Fork Combinator”), model checking for “stable coins”, and the development of a simulation package for networking code. This talk will describe the use of these methods at scale as part of the development of a large, complex, distributed system, the Cardano blockchain implementation. I will show the formal specification for the ledger code, show how it can be used to generate conformance tests using QuickCheck, and demonstrate consistency of the Haskell implementation.