I was formerly in the same lab as Leslie. As a side project, we (Tom Rodeheffer, mainly) used TLA to verify the correctness of Naiad's coordination protocol. The protocol is very simple (distributed reference counting), and my initial "proof sketch" was about two paragraphs long (and very unconvincing, apparently :). Tom's TLA+ version was closing in on 200 pages, available at
Very interesting, thanks (and to the other sibling poster).
> Tom's TLA+ version was closing in on 200 pages, available at [snip]
This is one of those things that I forgot to mention, namely the sheer amount of ambient knowledge we have embedded in our (not our computer's!) background knowledge of math and logical reasoning. Of course, sometimes we're actually wrong, so maybe we could stand a little double-checking by computer-based proof assistants, but I digress...
One thing that's also been mentioned in previous discussions I've been involved in and which is slightly worrying is that these kinds of languages tend to be quite anti-modular in that the proofs required for one type of system often don't transfer very well to other types of systems. (In general "algebra" proofs should probably transfer pretty well, but we're usually interested in very specific proofs for our systems.)
Aside: I wonder if Russel & Whiteheads's classic 1+1 proof has yet been (computer-)formalized?
Interesting. So perhaps we need some sort of "CTLAN" (Comprehensive TLA+ Tautology Archive Network?) kind of thing to be able to import/match obligations to already-established proofs from some common repository? Maybe future versions of TLAPS would benefit from such a thing?
(Sorry if this already exists; I'm just an interested layman.)
Damn; this is amazing stuff... I had no idea: (from [1]) so just get a local copy, set the path, and voila you can import... Wonderful. Thank you for sharing this!
for distributed protocols, you might want to try Alloy.
Basically it allows you to find counter examples (which are in this case scenarios).
http://www2.research.att.com/~pamela/zave_podc.pdf
is a well known example, working on the Chord join/leave protocol.
http://research.microsoft.com/pubs/183826/paper.pdf
A short publication about it, with some reflective discussion of why it was hard to write down, is at
http://research.microsoft.com/pubs/199767/clock-verif2.pdf
My understanding is that part of the problem was that Tom needed to explain (re-prove) many meta-facts we take for granted.