Lion: Modular Verification of Async Runtime Liveness
This work introduces an append-only logical event log that abstracts implementation details and enables a Kamp-style translation of Linear Temporal Logic into First-Order Logic, which enables deductive program verifiers to reason about progress via monotonic timestamps without needing native temporal logic support.