Is the database and/or specification open source? A formal verification of a distributed system sounds very interesting.
There's also a Coq framework called Verdi (http://verdi.uwplse.org) for formalizing distributed systems, but I don't know much about it.