Anatomy of a Lean proof for software engineers

..2026-10-01Anatomy of a Lean Proof for Software Engineers[Contents]IntroBackground: DFAs & Regular LanguagesDeterministic Finite Automaton (DFA)Regular LanguagesThe ProblemThe SolutionAdder ArithmeticAdder DFAExample 1Example 2The Lean ProofThe SpecificationThe ImplementationHow Proofs WorkThe ProofRun InvariantRun Invariant ProofBase CaseInductive StepSplitting the RunFirst Step AddsLeast Significant Bit SplitPutting It TogetherBRB^{\mathcal{R}}BR Is RegularAdder DFA Accepts BRB^{\mathcal{R}}B