I was referring to this claim from before the Jepsen report, which they have of course now quietly removed:
reply> ParticleDB’s home page advertised that ParticleDB was “formally proven” with a TLA+ proof. However, during our collaboration no TLA+ specification was available.
Makes you wonder if they asked their agent to formally prove it with TLA+ and it just responded that it had performed the proofing.
reply