Writing Security Invariants Got Easy. Keeping Them True Didn't.

In 2022, the first candidate on Alex Smolen’s list of security invariants was ‘all software services use single sign-on’. Four years on, a model can write that check in seconds. What it takes to keep it true — an engine, a seed of three files, and an honest place for exceptions — is the part worth designing.