Formal Verification: An Introduction through Elementary Arithmetic

Formal verification is often viewed as a highly specialized area accessible only to seasoned developers and researchers. Yet the core idea - verifying that an implementation satisfies a particular specification - can be introduced very naturally and easily via the basic arithmetic algorithms one learns in school.

In this talk I present a Lean 4 project that implements and proves the correctness of elementary pen-and-paper arithmetic algorithms, including addition, subtraction, multiplication, division, square-roots, and divisibility tests. Alongside the formal proofs, the project includes interactive visualizations that connect each step of an algorithm with the invariant or proof idea that justifies it. These visualizations allow users to follow both the execution of an algorithm and the invariants that justify its correctness.

The main purpose of the talk is to make formal verification more approachable using basic algorithms everyone already knows very well. Using these algorithms as case studies, the talk demonstrates how correctness invariants arise naturally from the mathematical structure of an algorithm and how inductive reasoning can be translated into machine-checked proofs in Lean.

• An accessible introduction to formal verification through familiar arithmetic algorithms.

• An understanding of how theorem-proving concepts such as induction and invariants arise naturally when reasoning about algorithm correctness

• An overview of how Lean 4 can be used to specify algorithms and construct machine-checked correctness proofs.

• An appreciation for how interactive visualizations can make formal verification and theorem-proving concepts more approachable.