> Liveness having to do with maintaining invariants over the lifetime of a computation. Nit: liveness is about reaching 'good' states over the lifetime of your

> Liveness having to do with maintaining invariants over the lifetime of a computation. Nit: liveness is about reaching 'good' states over the lifetime of your computation. If your invariant is violated, even if it's a multistate invariant, it's still a safety error. Liveness would be something like "x is eventually true", or "the program always terminates." It's not just specifications we need. We also need better tests. "Better" here doesn't mean "integration" or "acceptance", it means things like "fuzzing through contracts" or "comparing snapshots" or "rules-based state machines". Testing is vast and we're not very good at it.