We present a new approach for using a theorem-prover to verify the
correctness of protocols and distributed algorithms. The method
compares a state graph of the implementation with a specification
which is a state graph representing the desired abstract behavior.
The steps in the specification correspond to atomic transactions,
which are not atomic in the implementation.
The method relies on an {\em aggregation function}, which is a type of
an abstraction function that aggregates the
steps of each transaction in the implementation into a single atomic
transaction in the specification. The key idea in defining the
aggregation function is that it must {\em complete\/} atomic
transactions which have committed but are not finished.
We illustrate the method on a simple but nontrivial example. We have
successfully used it for other examples, including the cache coherence
protocol for the Stanford FLASH multiprocessor.