CSCI 1715

Formal Proof and Verification

Fall 2025

Course Description

Proof assistants are tools that are used to check the correctness of programs. Unlike tools like model checkers and SAT solvers, proof assistants are highly interactive. Machine-checked formal proofs lead to trustworthy programs and fully specified reliable mathematics. This course introduces students to the theory and use of proof assistants, using the system Lean. We will use Lean to verify properties of functional programs and theorems from pure mathematics. We will learn the theory of deductive reasoning and the logic that these tools are based on.

Syllabus: syllabus.pdf

Lecture: MW 9:30–10:50 AM, CIT 241

Office Hours: M 11-12 AM, CIT 203

Course Content

We plan to cover most of the Hitchhiker’s Guide to Logical Verification. We'll cover chapters roughly according to the schedule below, but topics may shift slightly as the semester progresses.

Assignments

Homework

Homework will be submitted via Gradescope. Please ensure that you have familiarized yourself with the grading and collaboration policies in the syllabus.

Homework Material Covered Released Due
HW 0 A quick survey 9/8/25 9/15/25
HW 1 Ch. 1, 2 9/8/25 9/17/25

Labs

Labs are optional, TA-guided sessions that provide an opportunity to practice and reinforce the content covered in lecture.

Lab Date

Lectures

You can view lecture demo files and view lecture recordings here. We will aim to update this table shortly after each lecture. All lecture recordings can also be found on Panopto.

Date Topic Resources Summary
9/3 Introduction Recording
Ch. 0 notes 		We'll talk about what Lean is and see what it can do, and also go over some organizational points about the course.

Takeaways: Verified programming is fun and powerful!
9/8 The basics of Lean syntax Recording
Ch. 1-2 notes 		In this lecture we'll learn the basics of the Lean programming and specification language: types and terms, type inhabitation, and writing and evaluating very simple functional programs. No proving yet!
9/10 Dependent type theory Recording
Ch. 1-2 notes 		We'll finish Chapter 2 of the HHG, and get a head start on some material from Chapter 4. Today's topics: inductive types (continued), function definition and evaluation, specifications, and dependent type theory.
9/15 Backward (tactic) proofs Recording
Ch. 3 notes 		We'll dive into the meat of the HHG Ch. 3: what are some of the moves available to us in the tactic proving minigame, beyond intro and apply? How do we deal with logical connectives: And, Or, Not, and so on?
9/17 Backward (tactic) proofs, contd. Recording
Ch. 3 notes 		We'll continue talking about tactic proofs. How do we deal with equality? What about the natural numbers? We'll also talk about classical vs constructive logic.

Calendar

Resources

CSCI 1715 Links

Lean Documentation & Search Tools

Lean Manuals

Community Resources

Staff

To email the course staff, click here. To email just the HTA and Rob, click here. To email Rob directly, click here. You are also encouraged to post (and answer!) questions on Ed Discussion.


Photo of Robert Y. Lewis

Robert Y. Lewis

Professor

Call me Rob! I'm half computer scientist, half mathematician, and fully excited to go through some of my favorite material with you all this semester. Pronouns: he/him/his

Photo of Chloe Qiao

Chloe Qiao

HTA

Hi! I'm a junior concentrating in computer science. When I'm not in the CIT, I enjoy rock-climbing, DDR, and building puzzlehunt sites. Pronouns: she/her/hers