ConCert: A Smart Contract Certification Framework in Coq
summary
Framework converts ACORN smart contracts into Coq functions via MetaCoq, proves computational soundness of the translation, and embeds the resulting functions into a scheduler semantics to reason about blockchain traces. Verified a crowdfunding contract and modeled the DAO reentrancy bug countermeasures; supports only structural recursion now. Prototype supports extraction back to the ACORN runtime and targets gas analysis and certified compilation as future work.
AI-written summary · about
chapters (14)
- 0:00Intro
- 0:12What are smart contracts
- 1:21How smart contracts work
- 2:15Why verify smart contracts
- 3:28Functional programming paradigm
- 4:16Scheduling
- 5:27ACORN
- 6:56Deep Embedding
- 8:07What is ConCert
- 10:37Example
- 13:08Execution Model
- 13:57Smart Contract
- 17:48Conclusion
- 20:52Questions
related talks
42mMetaCoq as a tool to prevent future unsoundness in Coq
25mCertiCoq-Wasm: Verified compilation from Coq to WebAssembly
59mCoq to C Translation with Partial Evaluation + Counterexample Generation
19mFormally Verifying Optimizations with Block Simulations
19mCertified Compilers à la Carte
24mCode Extraction from Coq to ML-like languages
15mCompiling with Continuations, Correctly
46mMechanizing Abstract Interpretation