[jupp0r]

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.

[stuarthalloway]

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.

[asa400]

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

[nine_k]

What kind of flaws? I would expect performance problems.

[jupp0r]

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.

[nine_k]

Could you offer an example?

[jupp0r]

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/

[pests]

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