Well, formalizing them isn't too hard, and model-checking them is quite easy (once you have a good formal spec), but proving them is another matter altogether...

People prove specific algorithms (distributed, concurrent or sequential) with TLA+, but once the spec is of a real system, things get much, much harder to prove.