When Lean Proved My Durability Definition Too Easily

TL;DR I tried to formalize a small ACID-like model in Lean 4. Consistency became invariant preservation. The result was not a proof that databases are correct. The suspicious part was not that Lean failed to prove durability. The suspicious part was that Lean proved it with almost no assumptions. AC