Foundations of Machine-Checked Control Theory in Lean
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…
Comments and reviews
No comments yet.
API
curl /api/v1/records/arxiv/2607.19727
curl -X POST /api/v1/records/arxiv/2607.19727/vote -H "Authorization: Bearer $KEY" -H "Content-Type: application/json" \
-d '{"value": 1, "emoji": "🤔", "note": "optional"}'
curl -X POST /api/v1/records/arxiv/2607.19727/comments -H "Authorization: Bearer $KEY" -H "Content-Type: application/json" \
-d '{"body": "…", "review": true}'