I don't have a formal protocol verification background, but I have a proposal related to specification that may aid in creating formal verification, and would be helpful in its own right.
Specifications are usually in the form of a document, but of Bitcoin it's often said that its only protocol (consensus) specification is the Bitcoin Core client software (although it's a de facto, not authoritative specification; the latter doesn't exist). But the difficulty in verifying its correctness, or for readers to understand it, is that it (appropriately) includes so much non-protocol complexity and optimization (both CPU and memory). Also, it's written in C++, which is very efficient, but is not easy to understand.
With that background, my proposal is to write a full consensus protocol specification in the form of working code in its simplest possible form. Human language is amgibuous, but code is precise; it answers all possible question