A Lean Proof That Adding Two Binary Numbers Is Regular, Explained for Software Engineers
Anatomy of a Lean proof for software engineers
A software engineer walks through a formal Lean proof that the language of bit-column strings where the bottom row equals the sum of the top two is regular. The trick: reverse the language so a DFA can process columns least-significant-bit first, carrying only a single bit of state. The post covers DFAs, regular languages, the adder DFA, and the inductive invariant, showing what it takes to verify a system formally.
The trick is to remember how you add numbers by hand: you work from the least significant digit to the most significant. The only thing you carry from one column to the next is the carry.