I don't think this is really surprising. I don't know a ton about distributed systems, but the last time I read up on formalizing them and proving properties it seemed like an incredibly daunting task. There's an exponential blowup problem in that you end up having to follow every state in the state spaces of every actor against every other state over time. I saw some interesting proofs which used topological invariants to keep a hold of that whole complex more delicately... but to actually just dive in and try exhausting it cannot be simple.

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.