Formally Verifying YUL Level Static Analyses and Optimization with Coq
summary
Provides a formally verified semantics for Yul-level (U-level) code in Coq, parametric by dialect with an almost-executable AVM dialect implementation and semantics operating on control-flow-graph level rather than SSA. Delivers a formally verified liveness checker that proves liveness results: if a variable is deemed dead, equivalent executions ignoring that variable still match. Work is exercised on a small corpus of contracts, used as a checker (not a full verified analyzer), and plans include broader contract coverage and adding A-level semantics for more analyses.
AI-written summary · about
chapters (11)
- 0:004U project introduction
- 0:21Formal verification for static analyzers
- 1:46Modeling analyzers in proof assistants
- 3:09Semantics in formal verification
- 4:33YUL semantics in Coq
- 5:56YUL semantics components
- 7:41Step and eval functions
- 8:02Liveness analysis verification
- 9:05Future plans and usability
- 10:08Q&A: Coq choice
- 10:29Q&A: Smart contract verification
related talks
23mVellvm: Formalizing the Informal
01h 06mVerifying a compiler through equational means
29mTowards Formally Verified Just-In-Time Compilation- 01h 06mVerifying a compiler through equational means
16mTowards formally secure compilation of verified F* programs against unverified ML(…)
01h 02mLanguage Design meets Verifying Compilers
31mPyrosome: A Framework for Modular, Extensible, Equivalence-Preserving Compilati...
21mEnhancing Symbolic Execution with Machine-Checked Safety Proofs