What are the limitations on formal proofs of Erlang systems? Well, today I just got my 15 minutes of fame, but now I think I am wrong on the point about formal proofs on Erlang systems.  The discussion on news.ycombinator.com suggests that Erlang code may or may not lend itself so well to formal reasoning (and it's certainly not pure a pure functional language), although a bit of google-fu turns up a fair number of peer reviewed articles on formal proofs on Erlang systems.

I'd like to get this right.  Can somebody here give a decent, in-depth explanation of the ins and outs of formal proofs on Erlang systems?
Erlang is a concurrent, higher-order programming language. To a decent approximation, this covers everything difficult about program verification. 

When a language is higher-order, the control structure of the program is not evident from the source code, since code are values, and so the control structure depends on the data flow in the program. When a language is concurrent, this means you have to reason about interference -- the possibility that multiple processes are trying to act on the same data at once. As a result, you have to think through all the possible interleavings of thread executions.  

Erlang is a reasonably clean language design, so it doesn't layer many  accidental difficulties on top of these two. But those two capabilities ensure that the essential difficulty is not easy. 

In fact, it's fair to say that the general problem of how to verify concurrent higher-order programs is still open --  proofs still tend to be tour-de-force efforts, rather than a systematic application of a methodology. We're a lot closer than we were five or ten years ago, though.