A formal framework for specification and verification of multi-agent systems is developed. Specification of an infrastructure created by a mobile agent platform is presented. On the basis of the specification, the notions of common ontology core, and agent’s knowledge are introduced. A simple agent architecture is presented. Given agents’ knowledge and decision mechanisms, model checking method is applied to verify whether the agents can realize their goals.