# Alloy Authors - Practical Alloy - Inductive invariants (Highlights) ![rw-book-cover|256](https://readwise-assets.s3.amazonaws.com/static/images/article2.74d541386bbf.png) ## Metadata **Review**:: [readwise.io](https://readwise.io/bookreview/51387478) **Source**:: #from/readwise #from/reader **Zettel**:: #zettel/fleeting **Status**:: #x **Authors**:: [[Alloy Authors]] **Full Title**:: Practical Alloy - Inductive invariants **Category**:: #articles #readwise/articles **Category Icon**:: 📰 **URL**:: [practicalalloy.github.io](https://practicalalloy.github.io/chapters/behavioral-topics/topics/inductive-invariants/index.html) **Host**:: [[practicalalloy.github.io]] **Highlighted**:: [[2025-05-13]] **Created**:: [[2025-05-14]] ## 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