Attempts to engineer autonomic multi-agent systems, particularly those having large numbers of agents, have revealed the need
for design structures and formalisms to support the construction of properties that emerge at the system level. Such emergence,
like self-∗ behaviour, relies typically on intricate inter-agent interactions. This paper shows how the top-down incremental
approach of Formal Methods can be used satisfactorily in that situation, by considering a case study in which agents adapt
and autonomously achieve a given configuration.