The environment is an essential component of multi-agent systems, which is often used to coordinate the behaviour of individual agents. Recently many programming languages have been proposed to facilitate the implementation of such environments. In this paper, we firstly introduce a formal setting which abstracts from concrete programming languages. We use this setting to show how concepts from mechanism design can be used to formally analyse and to verify whether specific normative behaviours can be enforced (or implemented) in a multi-agent system if agents follow their individual goals. We also consider complexity issues of associated problems.