LeanLTL: A unifying framework for linear temporal logics in Lean
Eric Vin, Kyle A. Miller, Daniel J. Fremont
cs.LO
Jul 2, 2025 · v1
TL;DR
Presents LeanLTL, a Lean 4 library unifying linear temporal logics with proof automation over finite and infinite traces.
Abstract
We propose LeanLTL, a unifying framework for linear temporal logics in Lean 4. LeanLTL supports reasoning about traces that represent either infinite or finite linear time. The library allows traditional LTL syntax to be combined with arbitrary Lean expressions, making it straightforward to define properties involving numerical or other types. We prove that standard flavors of LTL can be embedded in our framework. The library also provides automation for reasoning about LeanLTL formulas in a way that facilitates using Lean's existing tactics. Finally, we provide examples illustrating the utility of the library in reasoning about systems that come from applications.
Problem
Reasoning about linear temporal logic (LTL) properties of systems in a proof assistant requires ad-hoc encodings that do not unify different LTL variants or integrate well with the host language's native expressions.
Approach
LeanLTL provides a unifying Lean 4 library for linear temporal logics supporting both infinite and finite linear time traces. The library allows traditional LTL syntax to be combined with arbitrary Lean expressions, supports embedding of standard LTL flavors, and provides automation that leverages Lean's existing tactics.
Results
Standard flavors of LTL are proved embeddable in the framework. The library enables reasoning about systems from applications using native Lean tactics, with examples demonstrating utility for systems involving numerical and other types.
