Undo is a feature. Reversibility is a property.
The inverse is sealed before it lands. Anyone can check it afterwards — offline, and without trusting whoever issued it.
Three classes of failure sit outside what this covers — by declaration, not by oversight. Putting them here costs the first impression and saves you the afternoon you would otherwise spend discovering them.
| out of scope | why it cannot be closed from inside |
|---|---|
| Root or kernel-privileged writes | They go around the tool entirely, and this build does not detect that |
| Writes into the tool's own state directory | A detector living in that directory cannot judge it. The defence is an artifact held elsewhere |
| A policy that encodes the wrong intent | It will be enforced faithfully. No amount of verification reaches the question of whether the rule was right |
The full list ships in the repository, and a test fails if it drifts from the code that enforces it. The limits are not prose someone remembered to update.
| measured | under what conditions | |
|---|---|---|
| Test floor | 1,770 | probes across 318 suites · fresh clone · one machine · single run |
| Machine-checked | 90 | theorems, 0 sorry · three axioms carried, not proved |
| Open holes | 3 | high severity · adversarial round 13 · repair in progress |
| Not measured | 3 | Windows native, OneDrive, SMB — zero runs |
Numbers without the right-hand column are decoration. That column is why the table is wider than it looks like it needs to be.
No build badge — continuous integration is switched off, and a green tick would be a lie. No download counts and no star totals, because neither measures whether the thing works. Every figure above can be re-derived from the repository by someone who does not trust us.
