Securing HeyVL's Foundations in Lean

The paper "Securing the Foundations of an Intermediate Language for Probabilistic Program Verification" by Oliver Bøving and Christoph Matheja was published at ITP 2026 in Lisbon, Portugal.

The paper develops mechanized foundations in the interactive theorem prover Lean for proving the correctness of probabilistic-program verification techniques and their encodings in HeyVL. All results are built on top of mathlib.

The open-access paper is available online: "Securing the Foundations of an Intermediate Language for Probabilistic Program Verification".

Caesar makes it possible to rapidly prototype verification techniques by encoding programs, specifications, and proof rules in the quantitative intermediate verification language HeyVL. However, establishing that such an encoding is correct is subtle: the argument must connect HeyVL's denotational semantics to the probabilistic behavior of the encoded program.

The paper provides a machine-checked foundation for such arguments. In particular, it:

• formalizes Markov decision processes and constructs the probability spaces needed to give probabilistic programs an operational semantics;
• establishes least-fixed-point characterizations of expected total costs in Markov decision processes;
• derives sound weakest-precondition calculi for partial and total correctness, including unbounded loops, nondeterminism, and conditioning;
• develops a deep embedding of HeyVL in Lean; and
• uses this machinery to verify several existing HeyVL encodings.

The complete Lean formalization is available on Zenodo. For more background on HeyVL and Caesar's original formal foundations, see our OOPSLA 2023 paper "A Deductive Verification Infrastructure for Probabilistic Programs" and its announcement post.