You would possibly have a chance of modelling things like consensus with property-based testing by using stateful generators, which are covered later in the book. I know Chris Meiklejohn has had some success doing fault injection with fancier annotated models, though he eventually reoriented his stuff towards other forms of analysis.

While you can find errors and get more confident that specific execution paths are rather safe, a property test is not exhaustive and never represents an actual proof. Generally for protocols people will prefer to rely on formal specifications (like TLA+) at a higher level.

Much appreciated Fred – quite intriguing!

TLA+ (pronounced as tee ell a plus , /ˈtiː ɛl eɪ plʌs/) is a formal specification language developed by Leslie Lamport. It is used to design, model, document, and verify concurrent systems. TLA+ has been described as exhaustively-testable pseudocode,[4] and its use likened to drawing blueprints for software systems;[5] TLA is an acronym for Temporal Logic of Actions.

TLA+ 1
TLA+ 2

# Here’s a simple TLA+ specification, representing people trading unique items. Can you find the bug?
People == {"alice", "bob"}
Items == {"ore", "sheep", "brick"}
(* --algorithm trade
variable owner_of \in [Items -> People]

process giveitem \in 1..3 \* up to three possible trades made
variables item \in Items, 
          owner = owner_of[item], 
          to \in People,
          origin_of_trade \in People
begin Give:
    if origin_of_trade = owner then 
        owner_of[item] := to;
    end if;
end process;
end algorithm; *)

Leslie Lamport strikes again it would seem