Big claims about correctness and security keep failing inspection

Jepsen published 96 issues in ParticleDB 1.1.4, from crashes, deadlocks and data loss to partially invisible rows that couldn't be deleted and WHERE 4 = 5 misbehaving. The product's home page had advertised it as "formally proven" with a TLA+ proof. Separately, a TCP use-after-free (CVE-2026-98432, CVSS 9.8) affects Linux and apparently MikroTik routers, caused by the kernel handing saved options to a new connection without copying them and then freeing them. The advice is to watch for kernel updates and reboot. Air-gap leaking via radio signals from RAM and a thread on email encryption defaults, where servers don't verify certificates, rounded out the security mood.

The pattern: marketing says proven or secure, reality says otherwise, and the only reliable referee is someone adversarial. The air-gap and email threads make the same point from the other side, that assumed boundaries are weaker than they look.

There's some dry humor about "formally proven" being maybe "formerly". The joke lands because the gap between a spec and the running code is the actual problem.