Systems which exhibit emergent behaviour, i.e., behaviour not determined by the behaviours of the con-
stituents when considered in isolation, are becoming more common due to increasing use of distributed
and decentralised designs. There have been claims that formal methods, and particularly refinement, can
not be used to derive systems with emergent behaviour. In this paper, however, we argue that they can.
To prove the point, we perform a refinement of an oft-cited example of emergence: the ‘glider’ pattern
from Conway’s Game of Life.