Papers With

← All papers
First page of Foundations of Machine-Checked Control Theory in Lean

Foundations of Machine-Checked Control Theory in Lean

Moritz Doll, Iman Shames

math.OC Jul 22, 2026 · v1 cs.LO eess.SY
formalization verification analysis
Read PDF arXiv abstract
TL;DR
An open-source Lean/Mathlib library formalizes control theory, including Lyapunov stability and the small-gain theorem for cyber-physical system verification.
Abstract
We introduce an open-source library for machine-checked control theory in the interactive proof assistant Lean to lay foundations for the verification of cyber-physical systems. To this end, as representative theorems, we present formalizations of Lyapunov stability theory and the small-gain theorem. First, the machinery employed for formalizing Lyapunov stability, i.e., neighborhood filters, allows stating a Lyapunov theorem that covers both points and sets and applies to continuous, discrete, and hybrid systems. Second, the small-gain theorem is proved via stating input-output systems as relations without the usual well-posedness assumption. The Lean formalization of each of these theorems is then presented. We conclude by discussing the library architecture and mentioning some of the other system theoretic results that are formalized in the library along with future plans.
Problem

Verification of cyber-physical systems using proof assistants has been limited by the lack of formalized control theory. There is no comprehensive machine-checked library of dynamical systems and control results in Lean.

Approach

An open-source Lean library, LeanDynamicalSystems, is built on top of Mathlib to formalize control theory. Lyapunov stability is formalized using neighborhood filters, yielding a theorem covering points and sets across continuous, discrete, and hybrid systems. The small-gain theorem is proved by stating input-output systems as relations without the usual well-posedness assumption. The library is organized into Basic, mathlib, InputOutput, and Stability folders, with Verso-based documentation.

Results

Formalizations of Lyapunov stability theory (including LaSalle's invariance principle for sets and points) and the small-gain theorem are presented, along with definitions of causality, Lp-stability, and passivity. Example verifications include stability of the origin for x'=-rx and finite gain stability of a bounded multiplication operator. Missing topology and ODE lemmas are being upstreamed to Mathlib.