Sebastian Graf - Simpler do proofs with mvcgen

Stream: Lean Together 2026

[Rémy Degenne]

Discussion thread for the talk.

[Ching-Tsun Chou]

Are the slides of the presentation available somewhere?

[Ayhon]

Also, I had a question about the limits of the framework. In the slides it's stated as a goal to work with 90% of program logics out there. However, if I understood correctly, mvcgen and the Std.Do framework currently only manipulate monads, and proofs over them. Does this mean that monads are powerful enough to encode all interesting logics? Or is there some kind of limit to what can be encoded?