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.

▲

jen20 4 hours ago | parent [-]

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

	▲	foltik 3 hours ago \| parent [-]
		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.