What level would it be to use CSP or temporal logic to model the distributed system? I know you can use model checkers to find flaws in the design, but they work by searching the program state space instead of doing proofs, and so can only randomly find errors.
One of the papers related to Chubby (Paxos made live I think?) has a section about testing their implementation. At one point, they mention that their test suite was running for days before they found a rare bug in their implementation.
Level 4 on this list should probably be something about testing your implementation. Level 5 should be the creation of new algorithms (and making liveness and safety proofs for them). Level 6 should be complete mastery (or some other level which I’m not aware of yet).
To be really complete, something about using logs and basic database design should be included somewhere (system r, aries, etc).