I have a massive amount of respect for Martin and his work, but I think that this emphasis is the wrong one (if our goal is to increase the correctness of deployed distributed algorithms).
Instead, I like to think (building off work of folks like Ankush Desai, an AWS colleague and creator of P) that the process of specification, and it's products, are more valuable than the creation of a proof. Model checking - either exhaustive or stochastic - is valuable for checking the properties of specifications, but pushing the last step into full proof is often not worth the additional effort. Instead, I think making proof the focus and goal tends to turn most programmers off the whole topic.
I think we should be saying to folks "If you pick up these tools you'll end up with a crisp specification that'll help you move faster at development time, extremely clear documentation of your protocol, and a deeper understanding of what your protocol does" instead of "if you pick up these tools you'll end up with the mathematical artifact of a proof". This has been a big shift in my own thinking. When I first picked up Promela, Alloy, and TLA+/TLC/TLAPS, my own focus was on proof (and remained so until 2014 ish, when I spent a lot of time talking to Chris Newcombe and Leslie Lamport as we were writing the "Formal Methods at AWS" CACM paper). Over time I've found the journey much more valuable than the artifact, and tools like PlusCal and P which make specification more approachable more valuable than tools with less familiar syntax and semantics.
We shouldn't be surprised that few people can make progress when we ask them to understand both Paxos and Isabelle at the same time! Maybe if that's your focus as a PhD student, then it's OK.
> The real challenge in verifying distributed algorithms is to come up with the right invariant that is both true and also implies the properties you want your algorithm to have. Unfortunately, designing this invariant has to be done manually.
This is true. Invariants are hard. But maybe I'm more optimistic: I think that there are a lot of very real systems with straightforward invariants. Lamport's three invariants for consensus (section 2.1 of Paxos Made Simple), for example: https://lamport.azurewebsites.net/pubs/paxos-simple.pdf Similarly, invariants like Linearizability, and even formal definitions of isolation.
The research I would love to see is work to synthesize invariants from formalisms like Adya's or Crooks' work on database isolation levels. I think that's a very tractable project, and would be super useful to practitioners.