A system for specification and proof of distributed programs is presen
ted. The method is based directly on the partial order of local states
(poset) and avoids the notions of time and simultaneity. Programs are
specified by documenting the relationship between local states which
are adjacent to each other in the poset. Program properties are define
d by stating properties of the poset. Many program properties can be e
xpressed succinctly and elegantly using this method because poset prop
erties inherently account for varying processor execution speeds. The
system utilizes a proof technique which uses induction on the compleme
nt of the causally precedes relation and is shown to be useful in prov
ing poset properties. We demonstrate the system on three example algor
ithms: vector clocks, mutual exclusion, and direct dependency clocks.