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. ACID is familiar enough that it is easy to stop thinking about it. Atomicity. Consistency. Isolation. Durability. In ordinary database terms, the rough meanings are: Atomicity A transaction is all-or-nothing. It commits as a unit or has no effect. Consistency A transaction takes the database from one valid state to another valid state. Isolation Concurrent transactions behave as if they were controlled by some serial order. Durability Once a transaction commits, its effect survives failures and recovery.…