Specifying Smart Contract with Hax and ConCert
summary
A reproducible toolchain embeds Rust-style smart contracts into Hax, rewrites mutable state into message-passing state, annotates properties, and translates annotated code via Hax -> SSProof -> ConCert so cryptographic proofs (SSProof) cover individual functions and ConCert handles trace properties and QuickCheck testing. The pipeline extracts readable Rust (and Elm) code and already verifies realistic security properties for a non-smart-contract protocol; full mechanized proofs of end-to-end contract state evolution are not yet completed but the extraction-to-Rust and testing parts work.
AI-written summary · about
chapters (8)
- 0:00Smart contract formalization
- 1:49Smart contract languages
- 4:00Hax framework
- 6:52Security proofs with SSProve
- 8:40ConCert certification
- 10:50Multi-layer tooling
- 13:01Q&A
- 14:29Examples and future work
related talks
18mFormalising Decentralised Exchanges in Coq
29mCompositional Verification of Smart Contracts Through Communication Abstraction
15mCompositional Verification of Smart Contracts Through Communication Abstraction
54mMy Little Token (Part 1)
42mTotal Smart Contracts in Pact: Model-Verified Interfaces and Governance
30mConstructing Trustworthy Smart Contracts
21mPractical Verification Of Smart Contracts Using Memory Splitting
38mThe Duality of Smart Contracts and Electronic Rights