For more uptodate notes see http://www.cs.yale.edu/homes/aspnes/classes/465/notes.pdf.
(See Flooding for a simpler version of these notes that don't do IOAutomata.)
Let's define asynchronous broadcast to mean simulating the following AsynchronousBroadcast automaton with the following specification:
 AsynchronousBroadcast
 states
vectors sent: {0,1}^{{M}} and delivered: {0,1}^{{M×P}}, where M is the message set and P is the set of processes, initially all 0
 input actions

 send(m,p)
 effect: sent[m] := 1
 output actions
 deliver(m, p)
 precondition: sent[m] = 1, delivered[m,p] = 0; effect: delivered[m,p] := 1
 tasks
 each output action is a separate task
Note that this specification only delivers a message once no matter how many times it is sent. We have a separate send(m,p) action for each process p, because we want to allow a broadcast to start any any process (maybe even at more than one process); if there was a single send(m) action that was an input to all processes we'd have already solved in our model the problem we wanted to solve in practice.
We can simplify the specification further by observing that the AsynchronousBroadcast automaton is the composition of the following broadcast automata AsynchronousBroadcast_{m}, one for each m:
 AsynchronousBroadcast,,m,,
 states
 bit sent: {0,1} and vector delivered: {0,1}^{P}, where P is the set of processes, initially all 0
 input actions

 send(m,p)
 effect: sent := 1
 output actions
 deliver(m, p)
 precondition: sent = 1, delivered[p] = 0; effect: delivered[p] := 1
 tasks
 each output action is a separate task
Here's a distributed protocol for doing asynchronous broadcast in a weaklyconnected graph. What we'll do is define a separate DistributeAsynchronousBroadcast_{m}(p) automaton for each process p, and then argue that the composition of these automata together with a collection of reliable reordering channel automata for all p simulates AsynchronousBroadcast_{m}. If we want to simulate the full AsynchronousBroadcast automaton, we just compose together all the automata for all m.
 DistributedAsynchronousBroadcast,,m,,(p)
 states
 bit sent: {0,1} and vector delivered: {0,1}^{neighbors union {p}}, initially all 0
 input actions

 send(m,p)
 effect: sent := 1
 recv(p',p,m)
 effect: sent := 1
 output actions
 send(p, p', m)
 precondition: sent = 1, delivered[p'] = 0; effect: delivered[p'] := 1
 deliver(m, p)
 precondition: sent = 1, delivered[p] = 0; effect: delivered[p] := 1
 tasks
 each output action is a separate task
For completeness, we'll also throw in the ReliableReorderingChannel as a composition of messagespecific channels:
 ReliableReorderingChannel,,m,,(p,p')
 states
 counts sent: N and delivered: N, initially both 0
 input actions

 send(p,p',m)
 effect: sent := sent + 1
 output actions
 recv(p, p', m)
precondition: sent > delivered; effect: delivered := delivered + 1
 tasks
 each output action is a separate task
Now we'll do a simulation argument that shows that the composition of (a) DistributedAsynchronousBroadcast_{m}(p) for all p and (b) ReliableReorderingChannel_{m}(p,p') for all (p,p') in the graph simulates AsynchronousBroadcast_{m}. To avoid excessive typing, we'll drop the m's and abbreviate DistributedAsynchronousBroadcast_{m}(p) as Dp, ReliableReorderingChannel_{m}(p,p') as C(p,p'), and AsynchronousBroadcast_{m} as AB. The simulation map f sets AB.sent = max_{p} Dp.sent and AB.delivered[p] = Dp.delivered[p]. The simulation map ignores the contents of the channels
For the initial state s, we have f(s).sent = 0 and f(s).delivered[p] = 0 for all p, since all the Dp's are full of zeroes and we don't care about the state of the channels. We'd like to verify that it continues to work for all operations, but to do this we first need to prove some invariants:
 Channel input invariant
 C(p,p').sent = Dp.delivered[p'].
 Proof
Initially, both are 0. The only action that changes either value is send(p,p',m), which has precondition Dp.delivered[p'] = 0 implying C(p,p').sent = 0 by the invariant. After the operation, we set Dp.delivered[p'] := 1 and C(p,p').sent := C(p,p').sent^{old} + 1 = 1, so the invariant is preserved.
 Channel delivery invariant
C(p,p').delivered <= C(p,p').sent.
 Proof
 True initially, not affected by send(p,p',m), enforced by precondition of C(p,p') on recv(p,p',m).
 Channel output invariant
C(p,p').delivered <= Dp.sent.
 Proof
Again, it's true in the initial state. From the input and delivery invariants we have that C(p,p').delivered <= C(p,p').sent = Dp.delivered[p'] <= 1. So we only have to worry about what happens when C(p,p').delivered changes from 0 to 1 (=> recv(p,p',m) sets Dp.sent to 1 and preserves the invariant) or Dp.sent changes from 0 to 1 (possibly as the result of a different recv or send messageagain invariant is preserved because RHS increases).
 Process output invariant
Dp.delivered[p'] <= Dp.sent.
 Proof
 Yet another trivial variation of the preceding proofs.
From this we get the consolidated invariant Dp.sent >= Dp.delivered[p'] = C(p,p').sent >= C(p,p').delivered. (Technically we don't need the channel output invariant here, but we may need it later.) We can now show the simulation map works, by looking at the actions that change the state of some process. The easy part is showing that f(s).delivered[p] = s.Dp.delivered[p] works, because the only action that changes Dp.delivered[p] in the distributed system is deliver(p,m), and its precondition and effects in Dp line up exactly with the precondition and effects of deliver(p,m) in AB. Trickier is f(s).sent. There are two ways that f(s).sent could change from 0 to 1: either Dp.sent := 1 because of a send(m,p) operation (OK) or Dp.sent := 1 because of a recv(p',p,m) operation (maybe not OK). But in the latter case the precondition on recv(p',p,m) is C(p',p).sent > C(p',p).delivered >= 0 implying C(p',p).sent >= 1, and thus Dp'.sent >= C(p',p).sent = 1 in the previous state. This gives f(s).sent = 1 and so there is no change, allowing recv(p',p,m) to map to an empty trace.
So far we've just proved safety. To prove liveness, i.e. that every enabled deliver(m,p) operation eventually happens, we argue from the invariants that for every adjacent pair of processes (p,p') with Dp.sent = 1 and Dp.sent = 0, either Dp.deliver[p'] = 0 or C(p,p').sent > C(p,p').delivered. Then if {p': Dp'.sent = 0} is not empty, there is some p' in this set that is adjacent to a process p with Dp.sent = 1, and after some finite amount of time (a) p issues send(p,p',m) and (b) C(p,p') issues recv(p,p',m). At this point p' is added to the set. Repeating the argument gives that Dp.sent = 1 eventually for all p. It follows that deliver(m,p) is continuously enabled for any p that hasn't received the message yet, and so eventually it occurs by the fairness assumption.
(Comment: since only finitely many deliver(m,p) messages occur, we could weaken the task partition for AsynchronousBroadcast_{m} to put all deliveries of the same task in the same partition, and everything would still work.)