Total Smart Contracts in Pact: Model-Verified Interfaces and Governance

on YouTube ↗42m

" summary

Pact is a deliberately total, Turing‑incomplete contract language that puts source code on chain, adds an interactive REPL for local pact simulations, and wires properties into code so Z3 verifies invariants ahead of deployment. The uploader shows the Pact property checker using the Z3 SMT solver to find concrete counterexamples (e.g., same sender and receiver breaks mass‑conservation), and demonstrates capability‑based guards plus an upgrade governance mechanism that enforces who may upgrade modules and that the governance checks actually work.

AI-written summary · about

" chapters (12)

1. 0:00Start
2. 0:31Introduction
3. 0:58What Is Kadena
4. 2:38Why Pact
5. 4:26Rubik's Seed Bug
6. 6:58Type-Checking
7. 7:53Rebel Testing
8. 12:12Module Enforcement
9. 12:58Capabilities
10. 15:49Formally Verified Interfaces
11. 16:17Module Constraints
12. 22:21Enforce Account Admin

" related talks

• 54mMy Little Token (Part 1)Doug Beardsley · LambdaConf 2018
• 29mCompositional Verification of Smart Contracts Through Communication AbstractionArie Gurfinkel, Jorge A. Navas, Maria Christakis, Valentin Wüstholz, Scott Wesley, Richard Trefler · SPLASH 2022
• 15mCompositional Verification of Smart Contracts Through Communication AbstractionArie Gurfinkel, Jorge A. Navas, Maria Christakis, Valentin Wüstholz, Scott Wesley, Richard Trefler · SAS 2021
• 25mBehavioral simulation for smart contractsSidi Mohamed Beillahi, Constantin Enea, Michael Emmi, Gabriela Ciocarlie · SPLASH 2022
• 38mThe Duality of Smart Contracts and Electronic RightsDean Tribble · Web3 Summit 2018
• 23mGradual Verification for Smart ContractsJonathan Aldrich, Jenna Wise, Haojia Sun, Kunal Singh, Jan-Paul Ramos-Davila · PriSC 2024
• 16mSpecifying Smart Contract with Hax and ConCertBas Spitters, Lasse Letager Hansen · CoqPL 2024
• 51mA Deal with the Devil: Breaking Smart ContractsDavid Wong, Mason Hemmel · Black Hat Asia 2018