# Alloy Authors - Practical Alloy - Inductive invariants (Highlights) ![rw-book-cover|256](https://readwise-assets.s3.amazonaws.com/static/images/article2.74d541386bbf.png) ## Highlights - To be able to check these two conditions, we must first ensure that the initial state and events are not stated as facts, as facts may remove important behaviors. ([View Highlight](https://read.readwise.io/read/01jv5w0zvx8cmat6r3rk6se4f8)) ^889241455