A shallow dive into formal verification

vitalik.eth.limo · 6,104 words · saved by 8 readers

Over the last couple of months, a new programming paradigm has been rapidly gaining traction within Ethereum's frontier research and development circles, and many other corners of computing: writing code directly either in very low-level languages (eg. EVM bytecode, assembly language) or in Lean, and verifying its correctness with automatically-checkable mathematical proofs written in Lean. If done right, this has potential to both output extremely efficient code, and be far more secure than the way programming has been done before. Yoichi Hirai calls this the "final form of software development". This post will attempt to demystify the basics of what is going on here, what formal verification of software can do, and where its weaknesses and limits are, in Ethereum and beyond. Formal verification refers to writing proofs of mathematical theorems in such a way that these theorems can be checked automatically. To give a reasonably simple but still interesting example, let's take a basic

Dark Mode Toggle A shallow dive into formal verification 2026 May 18 See all posts A shallow dive into formal verification Special thanks to Yoichi Hirai, Justin Drake, Nadim Kobeissi and Alex Hicks for feedback and review Over the last couple of months, a new programming paradigm has been rapidly gaining traction within Ethereum's frontier research and development circles, and many other corners of computing: writing code directly either in very low-level languages (eg. EVM bytecode, assembly language) or in Lean, and verifying its correctness with automatically-checkable mathematical proofs

A shallow dive into formal verification

saved by

related reading