Overview of PROOF101

Welcome to the Introduction to Formal Verification & Proof Assistants course (PROOF101)! This collaborative initiative by the AUB Math Society introduces you to 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.

The 2027 edition will run over 14 weeks (two sessions per week), with a mandatory core track taught by the course instructor and a set of optional guest lecture tracks delivered by researchers from Boston University, Brown University, and so forth. While the course leans towards interactive theorem proving with Lean4, it is designed as a general introduction to formal verification, which also includes model checking, SAT/SMT solvers, and automated theorem provers (ATPs).

REGISTER HERE

Course Details:

• Primary Instructor & Organizer: Daniel Dia (dmd13@mail.aub.edu)
• Teaching Assistants: (to be announced) — quasi-weekly problem-solving sessions and office hours
• Organization: AUB Math Society
• Target Audience: ECE, CCE, CSE, CS, and other curious engineering/math (STEM) majors!
• Main Technology: Lean4
• Duration: 14 Weeks (2 sessions/week — one core lecture, one guest/track session, 1.5-2.0 hours each)
• Term: Monday 18 January 2027 — Wednesday 21 April 2027
• Format: Hybrid (in-person core lectures with live streamed & mostly recorded sessions; guest sessions online)
• Last Updated: August 27, 2026

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 | Week 11 | Week 12 | Week 13 | Week 14

Guest Lecture Tracks | Programming Assignments | Final Projects | Installing Lean4

Motivation: Why Proof Assistants?

Have you ever wondered how software failures and bugs, e.g. rocket malfunctions or medical devices that kill patients, could have been prevented? From the $370 million integer overflow (i.e. the Ariane 5 explosion) to the race condition that killed 3 patients (i.e. Therac-25), it is clear that 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 across the entire Internet actually!), and formalize Fields Medal-winning mathematics. Formal verification turns (very 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 interested in writing “bulletproof” software, a mathematician interested in formalized proof verification, or an engineer looking to build “safety-critical” systems, you’ll gain a lot from this 14-week course that will equip you with the tools and skills necessary for mathematically reasoning about programs. Course features include: assigned readings and interactive quizzes, six autograded Lean4 programming assignments, quasi-weekly problem-solving sessions run by our teaching assistants, and expert guest lectures from Dr. Assaf Kfoury and Dr. Marco Gaboardi (Boston University), Dr. Robert Lewis (Brown University), Rida Hamadani (LMAP, France), and Dr. Mohamad Sakr (American University of Beirut)!

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 such as PROOF100 (our dedicated preparatory course ran in Fall), CMPS211 (Discrete Structures), or EECE230 (Intro to Computation & Programming in Python) is very helpful, but not strictly required.

Course Structure: The Core Thread and the Tracks

PROOF101 runs on two layers, meeting twice a week.

Weekly rhythm:

• Monday, 15:00 — 17:00 — Core lecture (required)
• Wednesday, 15:00 — 17:00 — Guest/track session (optional, by track; open to all)
• Thursday, 16:00 — 18:00 — TA problem-solving session (quasi-weekly, optional but strongly recommended)
• Office hours — three slots spread across the week (instructor + both TAs)

Because no assignment, deadline, or core concept depends on a guest session, the track schedule can flex around our guests’ availability without ever disrupting your progress through the course.

Track sessions are open to everybody, regardless of what you declare. Declaring a track is a commitment to attend it, not a restriction on what else you may attend. Note also that the tracks are sequenced rather than parallel — Track A runs early, Tracks B and C run later, so a dedicated student can (and should!) realistically attend nearly all of them.

Guest Lecture Tracks

You must declare at least one track of A, B, or C by the end of Week 2 and attend at least 3 of its sessions.

Track A — Foundations: The Theory of Proof Assistants

The mathematical theory that makes proof assistants work, from the untyped λ-calculus to Lean 4’s kernel.

Guest Lecturers:

• Dr. Assaf Kfoury — Professor of Computer Science (Boston University) | Website
• Dr. Marco Gaboardi — Associate Professor of Computer Science (Boston University)

In fact, Dr. Kfoury and Dr. Gaboardi have previously delivered a lecture series titled “What Are Proof Assistants?”, “How To Use Them?”, and “Why Do They Work?”, which this track is largely based on.

Track B — Formalization in Practice

From a statement on paper to a finished Lean proof.

Guest Lecturers:

• Rida Hamadani (they/them) — Mathematical formalization researcher, former Lean Expert at Harmonic, Graduate student in resurgence theory (LMAP, France) | Website
• Dr. Robert Lewis — Assistant Professor of Computer Science (Brown University), instructor of CS1715 (Formal Proof and Verification) | Website

Track C — Automated Reasoning & Model Checking

The other side of formal verification: fully automatic techniques, what they can decide, and where they hit the wall.

Guest Lecturer:

• Dr. Mohamad Sakr — Assistant Professor of Computer Science (American University of Beirut)

Track D — Verification in the Wild (Research Colloquia)

Two research talks from researchers applying formal verification in industry and in safety-critical engineering.

Note: the colloquia are open to all students and count as bonus credit toward any declared track. Because there are only two of them, Track D does not on its own satisfy the track requirement.

Syllabus

Part 1: Foundations (Weeks 1-4)

Part 1 establishes what formal verification is about, why you should care about it, and introduces the foundational programming and mathematical concepts underlying proof assistants. Through real-world disasters and hands-on programming, we’ll see why exhaustive testing fails for safety-critical systems, learn to write real Lean4 code, and then build up the type theory that makes proof checking possible.

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

From Ariane 5 to Heartbleed: The High Cost of Software Bugs (Mon 18 Jan) · Lean4 Setup Lab & Track Fair (Wed 20 Jan)

We motivate the entire audience (especially software engineers and mathematicians) by showing the catastrophic failures of “correct-looking” code. Through 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 survey the full landscape of formal verification — automated and interactive alike. We close with an overview of the course structure and the four guest tracks.

Core Concepts:

• Real-world software disasters (case studies): Ariane 5 ($370M, integer overflow from reused code), Therac-25 (race condition, 6 deaths), Heartbleed (buffer over-read, 17% of servers exposed)
• Fundamental limitations of testing: finite inputs vs infinite possibilities, cannot test all executions/timing/concurrency, adversarial behavior, Dijkstra’s principle (testing shows presence of bugs, never absence)
• Formal verification foundations: mathematical proofs of program correctness, catching errors at compile-time, the spectrum from automated (SAT/SMT solvers, model checkers) to interactive (proof assistants with guaranteed soundness)
• Introduction to proof assistants: Rocq/Coq, Isabelle/HOL, Agda, Lean4, Curry-Howard correspondence (programs = proofs)
• Why Lean4: combines automation with verification guarantees, small trusted kernel (De Bruijn criterion ~10k lines), practical programming language, modern and actively developed, Mathlib mathematical library
• Dependent types (preview): types depending on values (Vector α n, Fin n, subtypes), encoding invariants directly in types, catching bugs at compile-time (“if it compiles, it’s correct”)
• What could have been prevented: turning catastrophic runtime crashes into compile-time type errors for all three disasters
• Course mechanics: the core thread, the four guest tracks, and how to choose one

Wednesday Session: Lean4 Setup Lab & Track Fair (run by the teaching assistants) — installing Lean4 and the VS Code extension, first .lean file, Gradescope walkthrough, joining the Lean Zulip, and a short introduction to each guest track.

Assignments & Further Study:

• Readings on formal methods and software security
• PROOF101 Quiz 1: Formal Verification Fundamentals
• Assignment 1: Setup & Community (due Sunday 24 January)

Week 2: Functional Programming

An Introduction to Functional Programming in Lean4 (Mon 25 Jan) · Track A1 (Wed 27 Jan)

We explore logic and programming paradigms as motivation (imperative, OOP, functional, etc.) and cover the basics of functional programming and typed functional programming in Lean4, following The Hitchhiker’s Guide to Logical Verification chapter 5. By the end of this week you will be writing recursive functions over lists and trees.

Core Concepts:

• Historical context (1936-2005): lambda calculus vs Turing machines (Church vs Turing, two models of computation), software crisis (1960s spaghetti code, GOTO statements), OOP dream vs reality (Smalltalk 1972 purity vs C++/Java corruption with mutable state), Tony Hoare’s “billion dollar mistake” (null pointers 1965), concurrency wall (2005, multicore requires immutability)
• Pure functions and side effects: deterministic (same input → same output), no observable side effects, benefits (cacheable via memoization, portable with explicit dependencies, testable without mocks, reasonable via referential transparency, parallelizable safely)
• First-class and higher-order functions: functions as values, map (transform each element), filter (select by predicate), fold (reduce to single value, foldr vs foldl), compose (chain functions)
• Currying and partial application: transform f:(α×β)→γ into f:α→β→γ, enables partial application, utility functions (curry, uncurry, flip, const)
• Inductive types in practice: enumerations (Weekday, Color), structures (Point with fields, functional update syntax), sum types (Sum α β with inl/inr), Option types (none/some, fixes the null pointer problem), recursive types (Nat, List, BTree)
• List and tree operations: map, filter, fold, zipWith, dropWhile, partition, interleave, splitAt, findIndex, tree operations (size, height, mirror, mapTree), tree traversals (inorder for BST, level-order breadth-first)
• Pattern matching and structural recursion: pattern matching on constructors (exhaustiveness checking), guaranteed termination, an informal first look at structural induction on lists and trees

Track Session (Wed 27 Jan): A1 — What are proof assistants, and why do they work? with Dr. Assaf Kfoury and Dr. Marco Gaboardi (Boston University)

Assignments & Further Study:

• Readings on functional programming
• PROOF101 Quiz 2: Functional Programming & λ-Calculus
• Assignment 2: Functional Programming in Lean (due Sunday 7 February)
• Declare your guest track by Sunday 31 January

Week 3: Types and Inductive Types (Dependent Types I)

Introduction to Lean4’s Type System (Mon 1 Feb) · Track A2 (Wed 3 Feb)

We gently introduce Lean’s type theory through The Hitchhiker’s Guide to Logical Verification chapters 1-2, covering types, terms, type inference, function definitions, and theorem statements. This is the first of a two-week sequence: this week we stay with simple and inductive types, and take our first look at the Curry-Howard correspondence.

Core Concepts:

• Lambda calculus foundations: λ-abstraction syntax (λx. M), β-reduction (function application), α-conversion (variable renaming), Church encodings (booleans, numerals as functions), higher-order functions (twice, compose), currying
• Simply typed lambda calculus: adding types for safety, type checking and inference, type judgments, function types, why types matter (catch errors, documentation, optimization)
• Types in Lean: basic types (Nat, Int, Bool, String), function types (right-associative), type constructors (List), product types (×), sum types (+), Option types (fixing null pointers), polymorphism with type variables
• Inductive types: natural numbers (Peano: zero, succ), lists (nil, cons), binary trees (empty, node), pattern matching, structural recursion (guaranteed termination), “no junk, no confusion” principle
• Curry-Howard correspondence (first pass): programs ↔ proofs, types ↔ propositions, → ↔ ⟹, × ↔ ∧, + ↔ ∨, type checking = proof checking
• Definitions, theorem statements, and reading Lean’s error messages

Track Session (Wed 3 Feb): A2 — Untyped λ-calculus: β-reduction, confluence and the Church–Rosser property with Dr. Assaf Kfoury and Dr. Marco Gaboardi

Assignments & Further Study:

• Readings on type theory
• PROOF101 Quiz 3: Types and Type Inference
• Continue Assignment 2 (due Sunday 7 February)

Week 4: Dependent Types and Lean’s Architecture (Dependent Types II)

Types That Depend on Values (Mon 8 Feb) · Track A3 (Wed 10 Feb)

The second half of our type theory sequence. We move from simple types to genuinely dependent types, see how invariants can be encoded directly in a type, and then open up the machine itself: how Lean’s elaborator and kernel divide the labour, and why that division is what makes the whole enterprise trustworthy.

Core Concepts:

• Dependent types: types depending on values (Vector α n, Fin n for bounded numbers, subtypes {x : α // P x}), dependent function types (Π-types), ∀x:σ, P(x) := (x:σ)→P(x)
• Encoding invariants in types: length-indexed vectors, safe indexing without runtime bounds checks, total functions by construction
• Barendregt’s λ-cube: the four corners of type dependency (terms on terms, terms on types, types on types, types on terms) and where Lean’s Calculus of Inductive Constructions sits
• Universes and Prop vs Type: proof irrelevance, why propositions live in their own universe
• Proof terms: what a proof is as a value, #check/#print, reading a term-mode proof
• Lean’s architecture: elaborator (untrusted, fills implicits/tactics) vs kernel (trusted ~10k lines, type checks all terms), the De Bruijn criterion (small trusted core), De Bruijn indices (variables as numbers, no alpha-conversion needed)

Track Session (Wed 10 Feb): A3 — The simply-typed λ-calculus and strong normalization with Dr. Assaf Kfoury and Dr. Marco Gaboardi

Assignments & Further Study:

• Readings on dependent types and Lean’s foundations
• Assignment 3: Types, Dependent Types & Proof Terms (due Sunday 21 February)

Part 2: Proving in Lean4 (Weeks 5-7)

Part 2 is where you start proving things. We build a practical toolkit of proof tactics — backward first, then forward — and then pause for a full week of consolidation, questions, and project planning. Tactic-based proving is core material this year, taught in the main thread, so that no student depends on a guest session for it.

Week 5: Tactic-based Proving I — Backward Proofs

Proving Your First Theorem (Mon 15 Feb) · Track B1 with Rida Hamadani (Wed 17 Feb)

We enter tactic mode and learn to work backwards from a goal, following The Hitchhiker’s Guide to Logical Verification chapter 3. We cover the introduction and elimination rules for every logical connective, the three kinds of equality, and the automation tactics that will save you hours.

Core Concepts:

• Tactic mode: the by keyword, the goal state, how tactics compile down to proof terms
• Basic tactics: intro, apply, exact, refine, assumption, and focus bullets (·) for structuring proofs
• Reasoning about logical connectives and quantifiers: And, Or, Not, Iff, Exists, ∀; introduction and elimination rules for each
• Reasoning about equality: three kinds (syntactic, definitional, propositional), the rfl tactic, rw/rwa, symm
• Decision procedures and automation: decide, omega, simp, simp_all, tauto, aesop, grind — and knowing when not to reach for them
• Case analysis: cases for decomposing disjunctions, by_cases for assuming a statement and its negation
• Reading and debugging a stuck goal state

Track Session (Wed 17 Feb): B1 — Hands-on proof-writing clinic with Rida Hamadani (LMAP, France): taking a statement on paper all the way to a finished Lean proof, live.

Assignments & Further Study:

• The Hitchhiker’s Guide to Logical Verification (Chapter 3)
• Continue Assignment 3 (due Sunday 21 February)
• Recommended: begin The Natural Number Game

Week 6: Tactic-based Proving II — Forward Proofs & Induction

Structured Proofs, Calculations, and Mathematical Induction (Mon 22 Feb) · Track A4 (Wed 24 Feb)

Backward proofs get you far, but readable proofs usually flow forwards. Following chapter 4 of the Hitchhiker’s Guide, we cover structured constructs, calculational reasoning, and mathematical induction — then tie it all back to the Propositions-as-Types principle.

Core Concepts:

• Forward reasoning: structured constructs (have, obtain, show, let), forward reasoning about connectives and quantifiers, mixing forward and backward styles within a single proof
• Calculational proofs: the calc keyword for chaining transitive relations, proving equalities and inequalities step by step
• Mathematical induction: the induction tactic with with | ... patterns, base case and inductive step, using the induction hypothesis, induction on lists and trees
• obtain for decomposing existentials and conjunctions
• The Propositions-as-Types (PAT) principle in practice: programs ↔ proofs, types ↔ propositions, tactics as proof-term constructors, #print on your own theorems
• Extensionality: function and set extensionality, the ext tactic
• Using library lemmas: exact?, apply?, searching Mathlib for what you need

Track Session (Wed 24 Feb): A4 — The Curry–Howard isomorphism with Dr. Assaf Kfoury and Dr. Marco Gaboardi. Deliberately scheduled immediately after PAT lands in the core thread.

Assignments & Further Study:

• The Hitchhiker’s Guide to Logical Verification (Chapter 4)
• Assignment 4: Tactic-based Proving (due Sunday 14 March)
• Start thinking seriously about your final project

Week 7: Consolidation, Concept Clinic & Project Proposals

Open Concept Clinic (Mon 1 Mar) · Project Proposal Workshop (Wed 3 Mar)

No new material this week. This is a deliberate mid-semester pause: a chance to catch up, ask about anything from Weeks 1-6 that didn’t land, and get your final project scoped properly while there is still plenty of time to build it.

Monday — Open Concept Clinic:

• Ask-me-anything on everything covered so far, with the instructor and both TAs
• Live re-proofs of the exercises that gave people the most trouble
• Common misconceptions: definitional vs propositional equality, implicit arguments, universe errors, why simp closed that goal and not this one
• Debugging clinic: bring your broken .lean file

Wednesday — Project Proposal Workshop:

• 3-minute idea pitches with live scoping feedback from staff and peers
• Is your project too big? Too small? Already in Mathlib?
• One-to-one slots with the instructor and both TAs
• Assignment of a TA mentor to each project

Assignments & Further Study:

• Continue Assignment 4 (due Sunday 14 March)
• Final Project Proposal due Sunday 7 March — LaTeX; title, overview, core property, anticipated challenges

Part 3: Verification in Practice (Weeks 8-11)

Part 3 turns proving into verifying. We introduce inductive predicates and rule induction, then use them to specify and verify real programs, learn the abstraction machinery that Mathlib is built from, and finally place Lean4 in the wider ecosystem of tools for reliable software. This part runs alongside Track C, where Dr. Mohamad Sakr covers the automated side of formal verification.

Week 8: Inductive Predicates & Rule Induction

Defining Properties Inductively (Mon 8 Mar) · Reserve Session (Wed 10 Mar)

Following The Hitchhiker’s Guide chapter 6, we learn to define properties — not just data — inductively, and to reason about them by induction on the proof rather than on the data.

Core Concepts:

• Inductive predicates: functions of type ... → Prop, introduction and elimination rules
• Worked examples: Even numbers (zero/add_two rules), Sorted lists, Palindrome, full binary trees, Permutation
• Logical symbols as inductive predicates: And, Or, Exists, and Eq (with only reflexivity as a constructor)
• Rule induction: structural induction on proof terms, and why it is the right tool for inductively defined properties
• Inductive predicates vs decidable functions: Decidable instances, when to define a Prop and when to define a Bool
• cases/rcases on inductive hypotheses, inversion principles

Wednesday (10 Mar): Reserve slot — held open as a buffer for guest rescheduling and for the Eid al-Fitr period. Any makeup session will be announced on Discord.

Assignments & Further Study:

• The Hitchhiker’s Guide to Logical Verification (Chapter 6)
• Assignment 4 due Sunday 14 March
• Proposal feedback returned; begin project development

Week 9: Specification & Program Verification

Proving That Programs Do What They Should (Mon 15 Mar) · Track A5 (Wed 17 Mar)

The heart of the course. Writing a program is easy; saying precisely what it should do is the hard part. We cover how to write honest specifications, and then verify a real algorithm end to end.

Core Concepts:

• What makes a good specification: total correctness, partial specifications, the “vacuous spec” trap (specifications that anything satisfies)
• Invariants: identifying them, stating them in Lean, threading them through a recursive definition
• Full worked case study: insertion sort is correct — the output is Sorted, and it is a Permutation of the input
• Proof engineering: decomposing a big theorem into have steps and auxiliary lemmas, naming conventions, when to generalize the induction hypothesis
• Termination and well-founded recursion: termination_by, decreasing_by, functions Lean can’t see are terminating
• Testing vs proving, revisited: #eval, decide, and property-based sanity checks as a complement to proof

Track Session (Wed 17 Mar): A5 — From the λ-calculus to Lean 4’s type theory: putting it all together with Dr. Assaf Kfoury and Dr. Marco Gaboardi. Concluding session of Track A.

Assignments & Further Study:

• The Hitchhiker’s Guide to Logical Verification (Chapters 8-9)
• Assignment 5: Inductive Predicates & Verified Programs (due Sunday 28 March)

Week 10: Structures, Typeclasses & Formalizing Mathematics

How Mathlib Is Built (Mon 22 Mar) · Track C-1 with Dr. Mohamad Sakr (Wed 24 Mar)

To formalize mathematics — or to write genuinely reusable verified code — you need abstraction. This session covers Lean’s structure/class/instance machinery and how the algebraic hierarchy in Mathlib is assembled from it.

Core Concepts:

• structure: fields, anonymous constructors, projections, functional update syntax, structures carrying proofs as fields
• Typeclasses: class, instance, instance resolution, variable [Group G], output parameters, why typeclasses and not just records
• Building a small algebraic hierarchy: Monoid → Group → AbelianGroup, and the diamond problem
• Decidable and DecidableEq instances: making decide work for your own types
• Navigating Mathlib: naming conventions, exact?/apply?/rw?, Loogle and the Mathlib docs, finding out whether a lemma already exists before proving it
• Reading Mathlib source: what a well-written formalization actually looks like
• Order duals (αᵒᵈ), coercions, and other things that will confuse you exactly once

Track Session (Wed 24 Mar): C-1 — Model checking: transition systems, temporal logic (LTL/CTL), and the state explosion problem with Dr. Mohamad Sakr

Assignments & Further Study:

• Mathematics in Lean 4 (Chapter 1 + at least one chapter of your choosing)
• Continue Assignment 5 (due Sunday 28 March)
• Project development continues

Week 11: Lean, Rust & the Verification Ecosystem

The Future of Reliable Software (Mon 29 Mar) · Track C-2 with Dr. Mohamad Sakr (Wed 31 Mar)

We tie the course together by placing Lean4 in the broader landscape, and look closely at Rust — a mainstream language whose type system is, in effect, a lightweight proof system that millions of engineers use without ever calling it that.

Core Concepts:

• The verification landscape revisited: Coq/Rocq (mature ecosystem, CompCert, Iris), Agda (flexible syntax, HoTT), F* (systems verification, verified crypto), Dafny (automatic verification, SMT-based), Isabelle/HOL (strong automation), and where Lean4 fits among them
• Rust’s ownership and borrowing: solving mutable aliased state via affine types (ownership) and region-safe aliasing (borrowing), the central invariant of any number of shared references (&T) XOR exactly one mutable reference (&mut T), preventing “spooky action at a distance” and iterator invalidation at compile time
• Lifetimes and Curry-Howard: lifetimes as region variables solving a constraint system over a partial order, traits as proof obligations checked at compile time, the borrow checker as an automated decision procedure for a fragment of intuitionistic linear logic
• Rust and the verification ecosystem: RustBelt proving semantic soundness in Rocq using Iris, the framing problem solved for free by the borrow checker, and tools like Aeneas translating mutable borrows into pure functions for verification in Lean4 without manual separation logic
• The cost/assurance spectrum: types → linters → model checkers → SMT-backed verifiers → proof assistants, and choosing the right point on it

Track Session (Wed 31 Mar): C-2 — SAT/SMT solving and automated theorem provers: what they can and cannot do with Dr. Mohamad Sakr

Assignments & Further Study:

• "Ownership" (by without.boats) and "References are like jumps"
• Assignment 6: Structures, Typeclasses & Mathlib (due Sunday 11 April)

Part 4: Advanced Tracks & Final Project (Weeks 12-14)

Part 4 hands the schedule over to our guests and to your projects. The core thread has finished, so the Monday slot opens up for additional track sessions while you build, prove, and document your final project with support from the course staff.

Week 12: Applied Verification & Contributing to Mathlib

Track C-3 with Dr. Mohamad Sakr (Mon 5 Apr) · Track B2 with Rida Hamadani (Wed 7 Apr)

Track Sessions:

• C-3 (Mon 5 Apr) — Applied verification: hardware, protocols, and industrial case studies, with Dr. Mohamad Sakr
• B2 (Wed 7 Apr) — Formalizing mathematics and contributing to Mathlib/CSlib, with Rida Hamadani: approaching a theorem from paper to Lean, navigating the library (modules, namespaces, hierarchies), the Blueprint system for large-scale formalization projects, the writing/testing/documenting/refining workflow, interacting with the Lean community on Zulip, finding a good first contribution, and real examples from merged pull requests

Assignments & Further Study:

• Mandatory project check-in (10 minutes per project with your TA mentor) — this week’s problem-solving session becomes a project clinic
• Continue Assignment 6 (due Sunday 11 April)
• Optional: browse recent Mathlib pull requests

Week 13: Metaprogramming, Decision Procedures & Research Colloquium

Track B3 (Mon 12 Apr) · Track B4 (Wed 14 Apr) · Colloquium D1 (Fri 16 Apr)

Track Sessions:

• B3 (Mon 12 Apr) — Metaprogramming and tactic design, with Dr. Robert Lewis: traditional tactics work by analyzing the proof state and (partially) assembling a proof term much like you could by hand. We implement the basic components of the interval_cases tactic this way, following a tutorial by Heather Macbeth, with exercises for interested participants.
• B4 (Wed 14 Apr) — Decision procedures, with Dr. Robert Lewis: two alternative strategies. Proof by certificate runs unverified code to generate a witness of the goal’s truth and then proves the certificate correct (linarith works this way); proof by reflection proves an algorithm correct in the object language and then wraps it in a thin layer of meta code. Cross-listed with Track C.
• D1 (Fri 16 Apr) — Research colloquium: formalizing polynomial commitment schemes and zkVMs at the Ethereum Foundation. Open to all students.

Assignments & Further Study:

• Assignment 6 due Sunday 11 April
• Track reflection due Sunday 18 April
• Optional dry-run presentations with the TAs
• Metaprogramming in Lean 4

Week 14: Research Colloquium & Project Showcase

Colloquium D2 (Mon 19 Apr) · Project Showcase, Competition & Wrap-up (Wed 21 Apr)

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

Monday — Colloquium D2: Formal verification in control systems. Open to all students.

Wednesday — Session Structure:

• 3-5 minute demos from all projects (with 2-3 minutes of questions)
• “Best Project” award (with great prizes!)
• Discussion on contributing to Mathlib or CSlib, and where to go from here
• Certificate of Distinction ceremony

Deadlines:

• Final project due at presentation time (Wednesday 21 April) — public or private GitHub repository, all .lean files compiling without errors, complete README.md

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 Course References

1. Mathematics in Lean

2. Metaprogramming in Lean 4

3. Undergraduate Mathematics in Mathlib

4. The Natural Number Game — interactive tutorial, part of Assignment 4

5. Track A (foundations): J. Roger Hindley, Basic Simple Type Theory (Cambridge University Press); Sorensen and Urzyczyn, Lectures on the Curry-Howard Isomorphism; and, for the ambitious, Jean-Yves Girard’s Linear Logic (TCS 50, 1987) and The System F of Variable Types, Fifteen Years Later (TCS 45, 1986). Contact Daniel Dia to obtain PDFs.

6. Track C (automated reasoning): Baier and Katoen, Principles of Model Checking; Bradley and Manna, The Calculus of Computation; the Handbook of Satisfiability

Additional Online Resources

• Lean4 Documentation
• Mathlib Documentation
• Lean Zulip Chat
• Lean Community

Installing Lean4

See our instructions on how to install Lean4. If your machine struggles with a local Mathlib build, we also provide a GitHub Codespaces configuration — ask on Discord.

Requirements & Policies

Programming Assignments

Throughout the course, you’ll complete six programming assignments that reinforce concepts through hands-on Lean4 programming. Assignments involve replacing sorry placeholders with working implementations and proofs, ensuring your code type-checks, and testing thoroughly. All assignments attach to the core thread — none of them require attending a guest session.

Submission and autograding: assignments are submitted to Gradescope and automatically graded — your submission is checked for sorry-free proofs of the correct type that use no nonstandard axioms. You will get immediate feedback and may resubmit. Because a failing autograder run is useful feedback, submit early and often. The pinned Lean toolchain shipped with each assignment skeleton must not be changed.

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.

Problem-Solving Sessions & Office Hours

Our teaching assistants run quasi-weekly problem-solving sessions (Thursdays, 16:00 — 18:00) that complement the assignments. These are not lectures and not solution sessions: expect one worked problem in the same shape as the assignment currently open, followed by live pair-proving with the TAs circulating. Sessions are keyed to the assignment you are currently working on, not to the lecture you just attended.

Office hours are offered in three slots across the week (instructor and both TAs) so that nobody waits more than about 48 hours for help. Times are published on Discord.

Track Requirement

• Declare one track by the end of Week 2 (Sunday 31 January)
• Attend at least 3 sessions of your declared track
• Submit a short track reflection (about half a page, due Sunday 18 April): what your track covered, one thing that changed how you think about the core material, and one open question. Pass/fail, read by the TAs.
• Attending sessions from other tracks is encouraged and counts as bonus credit

Certification

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

Core Requirements:

• Attend a minimum of 9 out of 11 core sessions
• Complete all online quizzes (Quizzes 1-3)
• Submit all six programming assignments, passing the autograder on at least four, and engage with the weekly assigned readings
• Complete one declared guest track (≥ 3 sessions) and submit the track reflection
• Complete and present a final mini-project during the Week 14 showcase

Note: Depending on the student’s performance and personal circumstances, some core requirements may be modified or dropped.

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

This year, proposals are due at mid-semester (Sunday 7 March) rather than in the closing weeks, giving you roughly six weeks of development time with a dedicated TA mentor — instead of the two weeks students had in Spring 2026. The Week 7 sessions are dedicated to scoping your idea properly before you commit to it.

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, past projects, and project ideas, 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:

• Dr. Assaf Kfoury (Boston University, US) — for ongoing support and guidance, and for anchoring the Track A lecture series
• Dr. Kinan Dak al Bab (Boston University, US) — for invaluable feedback, support, and coordinating our metaprogramming guest lecturer

Guest Lecturers:

• Dr. Assaf Kfoury and Dr. Marco Gaboardi (Boston University, US) — Track A: Foundations — The Theory of Proof Assistants (5 sessions)
• Rida Hamadani (LMAP, France) — Track B: hands-on proof-writing clinic and contributing to Mathlib/CSlib, and for offering to review Mathlib-related final projects
• Dr. Robert Lewis (Brown University, US) — Track B: metaprogramming in Lean and decision procedures
• Dr. Mohamad Sakr (American University of Beirut, Lebanon) — Track C: model checking, SAT/SMT solving, and automated theorem provers
• Research colloquium speakers (to be announced) — formalizing polynomial commitment schemes and zkVMs at the Ethereum Foundation; formal verification in control systems

Teaching Assistants:

• (to be announced) — for running the problem-solving sessions, office hours, the Gradescope autograding pipeline, and project mentoring

Organizational Support:

• AUB Math Society — for co-organizing this initiative and providing essential support

Design:

• Alina Gurskaya — for designing the course logo and visual materials

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:

• Share — copy and redistribute the material in any medium or format
• Adapt — remix, transform, and build upon the material

Under the following terms:

• Attribution — You must give appropriate credit, provide a link to the license, and indicate if changes were made
• NonCommercial — You may not use the material for commercial purposes
• ShareAlike — If you remix, transform, or build upon the material, you must distribute your contributions under the same license

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