Bringing the Power of Interactive Theorem Proving to Web3

Abstract

The security of the web3 ecosystem relies on the correctness of implementations of advanced mathematical formalisms, such as those underpinning various DeFi products or zk proof systems. The complexity of these formalisms, however, makes automated reasoning about said correctness challenging, if not intractable. In this talk, we give an overview of how some of these challenges can be tackled successfully in the world of interactive theorem proving. In particular, we focus on what it means to build an infrastructure for scalable reasoning about correctness of zk circuits, cryptographic algorithms, protocol models, and EVM/Yul-based smart contracts in the Lean proof assistant. Along the way, we give examples of how Nethermind was able to leverage such infrastructure in a number of real-world engagements.