[pka]

Is the database and/or specification open source? A formal verification of a distributed system sounds very interesting.

[pron]

No; not yet, at least. But this is a lecture series about using TLA+ for distributed algorithms: https://github.com/tlaplus/DrTLAPlus

There's also a Coq framework called Verdi (http://verdi.uwplse.org) for formalizing distributed systems, but I don't know much about it.

[pka]

Nice, thanks!