Programming with Proofs (November 2025)

• Instructor: Ilya Sergey

• Lectures: 18-22 November 2025

• Location: Neapolis University Pafos

Syllabus and Grading

• Syllabus and Policies
• Research Project: Guidelines and Deliverables

Course Materials

Course Textbook: The Hitchhiker’s Guide to Logical Verification (aka LoVe) by Baanen et al. Some of the lectures will be based on the materials of new work-in-progress class “Practical Verifications of Data structures and Algoritmms” (aka PraVDA).

Most of the lectures will be given using a white board and via live coding sessions.

Please, email me your GitHub handle (and your name) to have access to the repository containing the code for the lectures. To work on the exercises and assignments, please, create a private fork of the course repository.

Tentative Schedule

The course is structured as five lectures, each taking about 2.5-3 hours, including discussion and Q&A.

The timetable below is tentative and is subject to change.

	Lecture	Topics	Materials	Homework
1	Tue, Nov 18 6-9pm	Types, Programs, and Proofs	LoVe Chapters 1-3 LoVe Exercises 01, 02, 03	LoVe HW3
2	Wed, Nov 19 6-9pm	Functional Programming in Lean	LoVe Chapter 5 LoVe Exercises 05	LoVe HW5
3	Thu, Nov 20 6-9pm	Inductive Predicates Verifying Distributed Protocols in Veil	LoVe Chapter 6 LoVe Exercises 06 Veil verifier (slides) Veil examples (code)	LoVe HW6 PraVDA HW1
4	Fri, Nov 21 12-3pm	Mathematical Structures in Lean	LoVe Chapters 12-14 LoVe Exercises 12, 13, 14	LoVe HW12
5	Sat, Nov 22 12-3pm	Reasoning about Imperative Code Verifying Imperative Programs in Velvet	Floyd-Hoare logic (slides) Velvet examples (code)	PraVDA HW2

Software Prerequisites

Please, make sure to install Visual Studio Code and the following extensions and tools:

• Lean 4 theorem prover

• cvc5 SMT solver

• Z3 SMT Solver

You will need both cvc5 and z3 to be on your PATH to run some of the examples.

Additional Reading and Resources

On Lean

• Functional Programming in Lean

• Theorem Proving in Lean 4

• The Lean Language Reference

On Lean-based libraries discussed in the class

• Veil: a Verifier for Transition Systems (Veil repository)

• Velvet: a Verifier for Imperative Programs (Loom/Velvet repository)

• LeanSSR: an SSReflect-Like Tactic Language for Lean (LeanSSR repository)

Lean Community Zulip

• https://leanprover.zulipchat.com/

Copyright

Most of the basic materials for lectures 1-4 of this class are adapted, with permission, from the 2025 edition of the “Logical Verification” course developed by Anne Baanen, Alexander Bentkamp, Jasmin Blanchette, Xavier Généreux, Johannes Hölzl ,and Jannis Limperg. Slides on Hoare Logic are courtesy of Cesare Tinelli (University of Iowa).