The linked paper is quite interesting [0]. It does indeed sound like TLA+, the formal methods tool set they used, has worked out very well. One quote: "[W]e have found that software engineers more readily grasp the concept and practical value of TLA+ if we dub it: Exhaustively-testable pseudo-code. We initially avoid the words ‘formal’, ‘verification’, and ‘proof’, due to the widespread view that formal methods are impractical."

[0] http://research.microsoft.com/en-us/um/people/lamport/tla/fo...