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. Isolation became a deliberately strong commutation law. Durability exposed that my model had no persistence boundary. The result was not a proof that databases are correct. It was a reminder that every design claim depends on what the model can actually see. The suspicious part was not that Lean failed to prove durability. The suspicious part was that Lean proved it with almost no assumptions