Recent years have seen an enormous growth of interest in work at the intersection of logic and game theory. Forexample, researchers have used logic to make explicit the assumptions such as common knowledge that underpin many solution concepts, and have shown how solution concepts can be given a precise logical characterisation. From the perspective of computer science, these links open up the possibility of applying automated verification techniques, such as model checking, to the analysis and verification of computational mechanisms. We describe our work in this area, focussing on the use of game theoretic concepts in the specification and verification of coordination mechanisms for multi-agent systems.