Simpler $\texttt{do}$ proofs with $\texttt{mvcgen}$

Abstract: Since last year, $\texttt{Std}$ features $\texttt{mvcgen}$, a new experimental tactic that implements a monadic verification condition generator. It breaks down a goal involving a program written using Lean's imperative $\texttt{do}$ notation into a number of smaller $\textit{verification conditions}$ that are sufficient to prove the goal.

In this talk, we will go through a couple of examples that show how $\texttt{mvcgen}$ enables compositional reasoning where previous tactics fall short and have a look at its semantic foundations.

logic in computer science

Audience: advanced learners

( slides | video )

Lean Together 2026