Toy consensus

type node
type value
type quorum

relation member(N:node, Q:quorum)
axiom forall Q1:quorum, Q2:quorum. exists N:node. member(N, Q1) & member(N, Q2)

relation vote(N:node, V:value)
relation decision(V:value)

init ~vote(N,V)
init ~decision(V)

action cast_vote(n:node, v:value) = {
    assume ~vote(n,V);
    vote(n, v) := true
}

action decide(v:value, q:quorum) = {
    assume member(N, q) -> vote(N, v);
    decision(v) := true
}

export cast_vote
export decide

safety property:

conjecture decision(V1) & decision(V2) -> V1 = V2

inductive invariant:

conjecture vote(N,V1) & vote(N,V2) -> V1 = V2
conjecture decision(V) -> exists Q:quorum. forall N:node. member(N, Q) -> vote(N,V)

interpret quorum -> bv[2]
interpret node -> bv[2]
interpret value -> bv[2]