> before that it was formally verified
Jepsen is a fantastic tool - and one every database engineering team should have in their arsenal - but it proves the presence of bugs, not the absence of them. It is not formal verification, just a more rigorous form of existential testing.
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.
Makes you wonder if they asked their agent to formally prove it with TLA+ and it just responded that it had performed the proofing.