Beginner Resources for Program Verification in Lean ?

Stream: Program verification

[Alexander Kurz]

Hi, I am new to program verification in Lean (I have done work on program verification in Isabelle before). What are some good resources to get me started? I also would like to see examples of what has been done to get an idea of the state of the art.

[Mario Carneiro]

I would say that there is not really much material tailored for program verification. Perhaps the hitchhiker's guide #hglv (lean3) is useful? For the most part, proving theorems about programs is no different from any other kind of theorems in lean. There are some ideas for having a more streamlined experience in this situation but they have not yet materialized. But you can still reason about the definition of a function by cases or induction, use split liberally to break up match statements and so on. This is how most of the program verification theorems in Batteries are proved

[Alexander Kurz]

In the semester that just finished I taught a class based on the Lean NNG and the Logic Game to CS students ... https://hackmd.io/@alexhkurz/rJDrv_qDT ... this was just one 50 min session per week and some of the students were first year students, so we didnt get to program verification ... but I was very happy with how much the students learned, even if some of it must have remained mysterious to them. Anyway, I want to explore the possibilities of teaching a follow-up course about verification of programs in Lean.

[Martin Dvořák]

I like this chapter in the Lean 4 version of The Hitchhiker's Guide to Logical Verification:
https://browncs1951x.github.io/static/files/hitchhikersguide.pdf#page=147

[Miguel Raz Guzmán Macedo]

Thanks @Martin Dvořák , that's a very useful resource!

[Henrik Böving]

Note that the guide is being maintained by the theoretical cs group at LMU in this repo https://github.com/lean-forward/logical_verification_2024 it has slightly more updated things (since this is 2024 while the version linked above is 2023) and new stuff is likely to evolve there first. AFAIK the Brown version mostly differs in terms of the exercises provided with the book.