This is actually a very good point and unfortunately formal verification is not the current norm when developing DMBSs or complex systems software. If you asked how do you know DBMS X is correctly implementing snapshot isolation, no one will be able to provide a lesson for you. This is true for every system out there I'm aware of. This goes more deeply actually about questions like this: "how do you know you implement SQL or Cypher correctly". In fact, we can't even sometimes very formally answer "what is the meaning of this query X". Back in the day my PhD advisor Jennifer Widom, who had a background in programming languages, talked a lot about how we put DBMSs into everywhere, e.g., planes that are flying up in the air, yet we can't really precisely state what the outputs of queries should be. She had some excellent writing on this for implementation of triggers that were coming out of different groups. She was one of the pioneers of triggers before triggers existed in SQL. And as I assume you might know better than me, Leslie Lamport is known as a pioneer in the distributed systems space for formal verification of programs.

Your comment on shortened URLs is noted. This is my first HN post ever :), so I might need to pick up the customs.