Formal Verification of C# Smart Contracts

Explore formal verification techniques for C# smart contracts in this conference talk from NDC Oslo 2022. Delve into the critical importance of smart contract security in the blockchain industry, covering implementations of DAOs, tokens, NFTs, and DeFi services. Learn how formal verification can help detect bugs and vulnerabilities in smart contract code, with a focus on the Stratis blockchain platform and the Silver static analysis tool. Discover the unique suitability of smart contracts for static analysis and formal verification methods. Gain insights into blockchain fundamentals, the Stratis platform, C# smart contract environment, and the C# Roslyn compiler ecosystem. Examine the Silver command-line tool, Visual Studio Roslyn plugin, and techniques for statically analyzing .NET CIL code. Understand the Spec# programming system and its adaptation for modern C# using Roslyn source-code rewriters. Investigate various smart contract vulnerabilities and how formal verification addresses them through practical use cases.