Hacker News Reader

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

View on HN

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.

Reply on news.ycombinator.com