The theory of linear temporal properties – sets of system behaviours – including safety and liveness properties, as well as those described by linear temporal logics, is now well studied with many papers in the area. There are profound connections to topology as noted by Alpern and Schneider and more recently by Rayhana Amjad and Liam O’Connor in upcoming work.
Lean 4 is a proof assistant now popularly used by mathematicians, with many mature formalisations of topological concepts in mathlib. This project would involve developing a Lean library for linear-temporal reasoning, including connections to topology, formalisations of logic, and proof tactic tools.