We present a technique for checking aggregation abstractions
automatically using a finite-state enumerator.  The abstraction
relation between implementation and specification is checked
on-the-fly and the verification requires examining no more states than
checking a simple invariant property.  This technique can be used
alone for verification of finite-state protocols, or as preparation
for a more general aggregation proof using a general-purpose
theorem-prover.  We illustrate the technique on the cache coherence
protocol in the {\sc Flash} multiprocessor system.