What Is a ‘Liveness Property’ and How Does It Differ from an Invariant?

A liveness property is a condition that states "something good eventually happens," meaning the contract will eventually reach a desired state. It differs from an invariant (a safety property) which states "nothing bad ever happens." For a financial contract, a liveness property might be "a user who deposits collateral will eventually be able to withdraw it," or "the contract will eventually be upgradable." While invariants prevent loss, liveness ensures the contract remains functional and is not stuck in a permanent, unusable state.