Foundations of Machine-Checked Control Theory in Lean

Moritz Doll, Iman Shames

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…