Introduction to Formal Verification & Proof Assistants

A 10-Week Journey into Formal Verification with Lean4 (Spring 2026)

GDG @ AUB Software Team × AUB Math Society

PROOF101

Overview

Welcome to the Introduction to Formal Verification & Proof Assistants course (PROOF101)! This collaborative initiative between the GDG @ AUB Software Team and the AUB Math Society introduces you practical formal verification, the intersection of mathematics and programming, using the Lean4 proof assistant and programming language, which allows you to design and implement provably correct software systems.

Course Details:

Quick access to materials and important links:

Week 1 | Week 2 | Week 3 | Week 4 | Week 5 | Week 6 | Week 7 | Week 8 | Week 9 | Week 10

Motivation: Why Proof Assistants?

Ever wonder how software failures and bugs, like rocket malfunctions or medical devices that kill patients, could have been prevented? From the $370 million integer overflow (Ariane 5 explosion) to the race condition that killed 3 patients (Therac-25), catastrophic failures plague “correct-looking” code. To quote Edsger Dijkstra, “testing can show bugs exist, never their absence”. In PROOF101, we will teach you to mathematically prove your code is correct, not just exhaustively test it. We will study Lean4, an amazing proof assistant and programming language originally created by Microsoft Research, used to verify cryptography in Firefox and formalize Fields Medal-winning mathematics. Formal verification turns preventable catastrophic runtime crashes into compile-time errors, eliminating entire classes of bugs before they can cause any harm.

Whether you’re a computer scientist wanting to write “bulletproof” software, a mathematician interested in mechanized proof verification, or an engineer building “safety-critical” systems, you’ll gain a lot from this 10-week “crash course” (with the characteristics of a seminar) that will equip you with the tools and skills necessary for reasoning about programs with mathematical precision. Course features include: weekly interactive quizzes and assigned readings, occasional hands-on programming assignments in Lean4, and expert guest lectures from Dr. Rob Lewis (Brown University), Dr. Assaf Kfoury (Boston University), and Rida Hamadani (LMAP, France)!

Prerequisites: We essentially expect basic programming experience and familiarity with mathematical reasoning. No prior experience with functional programming or proof assistants required, since we’ll build everything from first principles, starting with the λ-calculus. Having completed courses equivalent to CMPS211 (Discrete Structures) or EECE230 (Intro to Computation & Programming in Python) is very helpful, but not strictly required.

Syllabus

Part 1: Foundations (Weeks 1-3)

Part 1 establishes what formal verification is about, why you should care about it, and introduces the foundational mathematical and programming concepts underlying proof assistants. Through real-world disasters and hands-on exploration, we’ll see why exhaustive testing often fails for safety-critical systems and how functional programming with dependent types provides a solution.

Week 1: Why Our Code Breaks (and How to Fix It)

From Ariane 5 to Heartbleed: The High Cost of Software Bugs (Wed 21 Jan)

We motivate the entire audience (especially software engineers and mathematicians) by showing the catastrophic failures of “correct-looking” code. Through a couple compelling case studies, including the Ariane 5 rocket explosion, the Therac-25 radiation machine, and the Heartbleed bug, we’ll examine the limits of testing and introduce the concept of formal verification as a path to (almost*) truly reliable software.

Core Concepts:

Assignments & Further Study:

Week 2: Dependent Types

Introduction to Lean4 and Dependent Type Theory (Mon 26 Jan)

We gently introduce Lean through The Hitchhiker’s Guide to Logical Verification chapters 1-2, covering types, terms, type definitions, type inference, function definitions, and theorem statements. This session also includes a brief overview of functional programming and begins a long introduction to λ-calculus that will continue in Week 3.

Core Concepts:

Assignments & Further Study:

Week 3: Functional Programming

An Introduction to Functional Programming in Lean4 (Mon 2 Feb)

We explore logic and programming paradigms as motivation (imperative, OOP, functional, etc.). Using Lean4, by applying what we have learned in week 2, we cover the basics of functional programming and typed functional programming through The Hitchhiker’s Guide to Logical Verification chapter 5.

Core Concepts:

Assignments & Further Study:

Part 2: Lean4 Fundamentals (Weeks 4-6)

Part 2 dives hands-on into Lean4. We’ll write our first proofs, understand the practical applications of dependent types, and build a practical toolkit of proof tactics. This section features guest lectures from Prof. Nadim Kobeissi and Rida Hamadani.

Week 4: Intro to Tactic-based Proving (Guest Session)

Proving Your First Theorem: An Introduction to Lean4 (Mon 9 Feb)

Guest lecturer Rida Hamadani, from the Laboratory of Mathematics and their Applications of Pau, will guide you through both backward and forward proof techniques in Lean4, covering The Hitchhiker’s Guide to Logical Verification chapters 3 and 4. We’ll explore the tactic mode, structured constructs, calculational proofs, and the Propositions-as-Types (PAT) principle.

Guest Lecturer:

Core Concepts:

Assignments & Further Study:

Week 5: Proofs & Semantics

Finishing up proof tactics and exploring formal semantics (Mon 16 Feb)

We’ll review backward and foward proofs in Lean4, introduce inductive predicates through The Hitchhiker’s Guide to Logical Verification chapter 6, and take a good look at operational semantics through chapter 3 (for culture, essentially).

Core Concepts:

Assignments & Further Study:

Week 6: Contributing to Mathlib (Guest Session, AUB Math Society)

Formalizing Mathematics and Contributing to Mathlib (Wed 25 Feb)

Co-organized with the AUB Math Society, this hands-on session by Rida Hamadani will show you the complete workflow of mathematical formalization in Lean4: from reading a theorem on paper to contributing verified mathematical proofs to Mathlib or CSlib. Learn how to navigate the library, find existing theorems, use the Blueprint system for large-scale formalization projects, and interact with the Lean community effectively.

Guest Lecturer:

Core Concepts:

Assignments & Further Study:

Part 3: Real-World Applications (Weeks 7-8)

Part 3 connects proof assistants to real-world applications. We’ll see how formal verification is used in high-assurance cryptography and explore advanced metaprogramming techniques including monads, custom tactics, and automated decision procedures.

Week 7: Mathematical Foundations of Proof Assistants (Guest Session)

The Type-Theoretic Foundations That Make Proof Assistants Possible (Mon 9 March)

This session bridges the pragmatic use of Lean with the mathematical theory (i.e. type theory) that makes proof assistants work. Building on prior weeks’ hands-on experience with tactics and functional programming in Lean4, we will learn about the foundations of type theory, the Curry-Howard isomorphism between proofs and programs, and algorithms for type inhabitation and counting.

Core Concepts:

Assignments & Further Study:

Week 8: Monads, Tactics, and Applications

Advanced Metaprogramming and Decision Procedures (Mon 16 March)

Dr. Rob Lewis from Brown University will guide us through different strategic approaches to tactic design, from direct proof manipulation to sophisticated decision procedures, with a deep dive into how tactics like linarith work under the hood.

Guest Lecturer:

Core Concepts:

Assignments & Further Study:

Part 4: Final Project & Next Steps (Weeks 9-10)

Part 4 is dedicated to your final project. You’ll apply everything you’ve learned to verify a small but meaningful property, with dedicated support from session leaders and the opportunity to showcase your work.

Week 9: The Broader Landscape & Project Kick-off

Lean, Rust, and the Future of Reliable Software (Wed 23 March)

We tie all concepts together and launch the final project. You’ll understand how Rust’s borrow checker acts as a “proof system,” survey other tools in the landscape (Rocq/Coq, Agda, F*), and begin brainstorming your own verification project.

Core Concepts:

Assignments & Further Study:

Week 10: Project Showcase & Wrap-up

Project Showcase, Competition, and ‘Where to Go From Here’ (Wed 1 Apr)

Celebrate your achievements! Every project gets a 5-10 minute demo, we award “Best Project,” discuss contributing to Mathlib, and present all Certificates of Distinction. This is just the beginning of your formal verification journey!

Session Structure:

Resources

Course Textbooks

All course textbooks are freely available online:

  1. The Hitchhiker’s Guide to Logical Verification
    Structured concise textbook covering proof assistants and formal verification (PDF).

  2. Theorem Proving in Lean 4
    The primary course reference for Lean4 syntax, tactics, and proof techniques.

  3. Functional Programming in Lean 4
    Comprehensive guide to functional programming concepts in Lean4.

Additional Resources

Installing Lean4

See our instructions on how to install Lean4.

Requirements & Policies

Programming Assignments

Throughout the course, you’ll complete 4 programming assignments that reinforce concepts through hands-on Lean4 programming. Assignments involve replacing sorry placeholders with working implementations, ensuring code type-checks, and testing thoroughly.

PROOF101 maintains a strict zero-tolerance policy for academic dishonesty. Copying work, sharing solutions, or use of LLMs unacknowledged is prohibited and will result in zero credit and ineligibility for certification.

For complete guidelines, submission instructions, and academic integrity policies, see the Programming Assignments page.

Certification

Certificate of Distinction: Participation is open to all, but certification is reserved for those who demonstrate mastery.

Core Requirements:

Final Projects

Your final project demonstrates mastery by applying formal verification to a topic you care about. Choose between:

  1. Mathematical Track: Formalize a theorem and its proof
  2. Algorithmic Track: Verify properties of an algorithm or data structure

Optional: Some students may choose to contribute to Mathlib or CSlib as their project, with guidance and review from Rida Hamadani.

For complete project requirements, guidelines, and examples, see the Final Projects page.

Acknowledgments

This course would not have been possible without the generous support and contributions of many individuals and organizations.

Special Thanks to Our Faculty Mentors:

Guest Lecturers:

Organizational Support:

Design:

And to all participants who bring energy, curiosity, and dedication to making this learning community thrive.

For a complete list of contributors to the course materials, see our PROOF101 “Contributors” page.

License

Introduction to Formal Verification & Proof Assistants (PROOF101) by Daniel Dia and contributors is licensed under Creative Commons Attribution-NonCommercial-ShareAlike 4.0 International.

This means you are free to:

Under the following terms:

For the complete license text, visit: https://creativecommons.org/licenses/by-nc-sa/4.0/legalcode