Formal verification of C# smart contracts
summary
Shows concrete verification of C# smart contracts on Stratis using the Silver static analyzer and Spec#-style annotations rewritten via Roslyn into a Boogie pipeline. Verifies at source and .NET CIL level, flags disallowed APIs and heap allocation, and catches real bugs — e.g. a donate method that fails verification until the transfer return value is checked, and a reentrancy-precondition that forces explicit checks. Runs as a Visual Studio analyzer or CLI for CI, processes GitHub PR assemblies, and emits proven/failed method results.
AI-written summary · about
chapters (10)
- 0:00Formal verification intro
- 4:41Stratus platform basics
- 11:37Smart contract security
- 20:33Static analysis with Silver
- 21:59Formal verification theory
- 31:20Integrating formal specs
- 33:08Spec# verification pipeline
- 37:30Detecting vulnerabilities
- 41:46Re-entrancy mitigation
- 45:19Summary & Q&A
related talks
30mVerifying Solidity Smart Contracts Via Communication Abstraction in SmartACE
06mFormal Verification with the Certora Prover
25mBehavioral simulation for smart contracts
14mRich Specifications for Ethereum Smart Contract Verification
30mConstructing Trustworthy Smart Contracts
54mContinuous Integration: Live Static Analysis using Visual Studio & the Roslyn API
50mTrust but Verify: Scaling Deductive Verification with Abstract Interpretation
07mV for Verification