Smart Contracts and Formal Verification with Z3 with Pact

Stuart Popejoy introduces Pact, a Turing-incomplete smart contract language built in Haskell, and demonstrates its formal verification capabilities using Z3.

Stuart Popejoy C◦mp◦se :: Conference composeconference.org/2017/ May 19, 2017 We present Pact, a new open-source language for authoring smart contracts, built in Haskell. Smart contract languages like Ethereum’s Solidity have taken a maximalist approach to functionality, in no small part because the slow execution speed of public blockchains emphasizes “feature-rich” transactions that compose multiple invariants into a single transaction. Resulting logic is complex, brittle, and often incorrect. With Pact, a high-performance blockchain ensures that transactions can closely model business invariants, and “fail fast” on invalid cases or retry scenarios. Logic is constrained to Turing-incomplete (terminating) execution and single-assignment (immutable) variables. We discuss the unique hybrid of strict OLTP workload and limited key-value querying needed for blockchain applications, and how this informs Pact’s database model. We also discuss the influence of Bitcoin scripts on Pact’s design as well as its integration of public-key authorization schemes. We demonstrate various Pact smart contracts running both in a standalone interpreter as well as in the ScalableBFT blockchain. Finally, we give a demo of static analysis and verification using the Z3 theorem prover, and show the new development environment with a sample application.