I was referring to this claim from before the Jepsen report, which they have of course now quietly removed:

> ParticleDB’s home page advertised that ParticleDB was “formally proven” with a TLA+ proof. However, during our collaboration no TLA+ specification was available.