Design verification using TLA+ and Alloy is a completely different game than verification at the level of code as in Verdi. While there are plenty of studies saying design verification is good in general, I'm not aware of any studies saying that (or quantifying to what degree) it gets you close to implementation verification. On the flip side, the classic paper on the implementation of Paxos hints at just at how wide the gap is between design and running systems: https://research.google.com/archive/paxos_made_live.html
While Frama-C style verification works well out-of-the-box for proving single-threaded, isolated programs correct, one has to make a major effort to capture assumption-heavy distributed systems behavior using ghost code and other tricks. The only effort I'm aware of in this direction is the following, which uses the VCC tool: http://madhu.cs.illinois.edu/evcons.pdf
While Frama-C style verification works well out-of-the-box for proving single-threaded, isolated programs correct, one has to make a major effort to capture assumption-heavy distributed systems behavior using ghost code and other tricks. The only effort I'm aware of in this direction is the following, which uses the VCC tool: http://madhu.cs.illinois.edu/evcons.pdf