In practical terms, if you are a database and Jepsen doesn't find any bugs, that's as much assurance as you are going to get in 2024 short of formal verification.

Formal verification is very powerful but still not full assurance. Fun fact: Testing and monitoring of Datomic has sometimes uncovered design flaws in underlying storages that formal verification missed.

Is there anything I can read about what capabilities Datomic requires of the underlying storages it uses?

What kind of flaws? I would expect performance problems.

To start with, you usually perform verification on a behavioral model and not on the code itself. This opens up the possibility that there are behavioral differences between the code itself and the model which wouldn't be caught.

Could you offer an example?

If you work through the TLA+ tutorial[1] it will help you get a good idea of the benefits and limitations of verification.

[1] https://learntla.com/

The work antithesis has been doing here has me really excited as well.

That's consistent with the usual definition of "finding" anything.

"Absence of evidence is not evidence of absence."

Thank you. I've updated my initial guess of p(critical bugs | did not find critical bugs) from 0.5 to 0.82 given my estimate of likelihood and base rates.

If you've looked, it is. The more and the better you look, the better evidence it is.

If a test almost always finds something, then the failure of that test to find something is strong evidence.

s/evidence/proof/.

Evidence of absence ("we searched really carefully and nothing came up") does update the Bayesian priors significantly, so the probability of absence of bugs can now be estimated as much higher.