> 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.