Distributed reference counting is a general purpose technique, which may be
used, e.g., to detect termination of distributed programs or to implement
distributed garbage collection. We present a distributed reference counting
algorithm and a mechanical proof of correctness carried out using the proo
f assistant Cog. The algorithm is formalised by an abstract machine, and it
s correctness has two different facets. The safety property ensures that if
there exists a reference to a resource, then its reference counter will be
strictly positive. Liveness guarantees that if all references to a resourc
e are deleted, its reference counter will eventually become null.