Authoring and Formal Verification of Smart Contracts in Pact
summary
A property checker for Pact translates Pact programs and properties to SMT constraints and hands them to Z3 SMT solver, implemented via SBV/Haskell. It proves schema invariants and function properties like purity and absence of aborts, finds concrete counterexamples, and catches real bugs such as negative balances or violated mass conservation. It returns results quickly on real contracts but limits include partial language coverage, no verified checker, and potential scalability risks as properties become more expressive.
AI-written summary · about
chapters (18)
- 0:00Start
- 0:28Pact: introduction
- 1:55Pact: tables
- 2:23Pact: a function
- 3:20Pact: optional types
- 4:01Pact: enforcing an invariant
- 4:12Property checker motivation
- 5:41Liquid Haskell?
- 5:59Ada / SPARK
- 6:47Manticore
- 7:23The Pact property checker
- 8:55Schema invariants
- 9:17Function properties
- 9:56The mass conservation property
- 24:28How does it work?
- 26:20Limitations
- 28:24Roadmap
- 30:25Joel Burget - joel@monic.co
related talks
30mVerifying Solidity Smart Contracts Via Communication Abstraction in SmartACE
54mProperty Based Testing - Smart testing of smart contracts
06mFormal Verification with the Certora Prover
58mAutomating Relational Verification of Infinite-State Programs
25mBehavioral simulation for smart contracts
46mFormal verification of C# smart contracts
14mRich Specifications for Ethereum Smart Contract Verification
21mPractical Verification Of Smart Contracts Using Memory Splitting