Examples

Stream: Program verification

[Дмитрий Лейкин]

Hi Everyone,
I'm software developer. Is there any examples of program verification using Lean, or tutorials, that can be used for learning? Not to prove theorems about math, but theorems about code to prove it's correctness? Now I found only https://kqueue.org/blog/2020/10/15/arithcc/ (which was very helpful for learning).

[Anne Baanen]

We're teaching a course on formal verification in Lean at the moment :)

[Johan Commelin]

@Дмитрий Лейкин Also note that Lean 4 will probably make program verification a lot more pleasant compared to Lean 3.