To specify the design of operating systems and other “systems level” software, it’s possible to use temporal-logic style qualifiers like “always” or “eventually” or more detailed similar qualifiers in just ordinary algebra and state machines.
https://www.yodaiken.com/wp-content/uploads/2025/10/temporal.pdf
temporal
Specifications like temporal logic but with ordinary mathematics