Comment by foltik
16 hours ago
Ok sure, so an LLM told you all the bugs are fixed and it’s faster than Redis, just like how it told you before that it was formally verified?
Please try to resist the urge of being a meat proxy.
16 hours ago
Ok sure, so an LLM told you all the bugs are fixed and it’s faster than Redis, just like how it told you before that it was formally verified?
Please try to resist the urge of being a meat proxy.
> 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.