# CertRL: Formalizing Convergence Proofs for Value and Policy Iteration in Coq

arXiv: https://arxiv.org/abs/2009.11403 · HTML: https://mlsanity.com/paper/2009.11403/

## Key facts

- Cited by 9 papers in the map (data through 14 Oct 2026).
- First posted on arXiv 23 Sep 2020.

## Built on by (most cited first, 9 of 9)

- [Towards Formalizing Reinforcement Learning Theory: A Robbins-Siegmund Approach](https://mlsanity.com/paper/2511.03618/) (2025)
- [Formalization of a Stochastic Approximation Theorem](https://mlsanity.com/paper/2202.05959/) (2022)
- [Formalising the Foundations of Discrete Reinforcement Learning in Isabelle/HOL](https://mlsanity.com/paper/2112.05996/) (2021)
- [Lean Formalization of Generalization Error Bound by Rademacher Complexity and Dudley's Entropy Integral](https://mlsanity.com/paper/2503.19605/) (2025)
- [Formalized Hopfield Networks and Boltzmann Machines](https://mlsanity.com/paper/2512.07766/) (2025)
- [Formally Verified Approximate Policy Iteration](https://mlsanity.com/paper/2406.07340/) (2024)
- [Formally Verified Solution Methods for Infinite-Horizon Markov Decision Processes](https://mlsanity.com/paper/2206.02169/) (2022)
- [Coinductive guide to inductive transformer heads](https://mlsanity.com/paper/2302.01834/) (2023)
- [Working Paper: Towards Schema-based Learning from a Category-Theoretic Perspective](https://mlsanity.com/paper/2604.10589/) (2026)

## Abstract (arXiv)

Reinforcement learning algorithms solve sequential decision-making problems in probabilistic environments by optimizing for long-term reward. The desire to use reinforcement learning in safety-critical settings inspires a recent line of work on formally constrained reinforcement learning; however, these methods place the implementation of the learning algorithm in their Trusted Computing Base. The crucial correctness property of these implementations is a guarantee that the learning algorithm converges to an optimal policy. This paper begins the work of closing this gap by developing a Coq formalization of two canonical reinforcement learning algorithms: value and policy iteration for finite state Markov decision processes. The central results are a formalization of Bellman's optimality principle and its proof, which uses a contraction property of Bellman optimality operator to establish that a sequence converges in the infinite horizon limit. The CertRL development exemplifies how the Giry monad and mechanized metric coinduction streamline optimality proofs for reinforcement learning algorithms. The CertRL library provides a general framework for proving properties about Markov decision processes and reinforcement learning algorithms, paving the way for further work on formalization of reinforcement learning algorithms.