Journal of Information Organization Hina Faryal 4 2 2014 A multi-agent system is used to solve problem that is difficult or impossible to solve by centralized system. Our multi-agent system provides a system that is formally verified. We have analyzed the development process of a multiagent system after classifying it in the major phases of formal verification specifications, architecture specifications and implementation. Formal verification helps confirm that your software models and code behave correctly. We are using Formal model-checking approaches for the architecture and verification specifications. Formal verification, architecture, and implementation of an excursionist multi-agent system are implemented by using JADE (Java Agent Development Framework). JADE is a software framework fully implemented in Java language. It simplifies the implementation of multiagent systems with FIPA specifications and through a set of graphical tools that supports the debugging and deployment phases. This multi-agent system informs a user about their exact location, and guides him to find other locations (i.e. faculties, offices, hostels, banks, other buildings etc) inside the Bagdad-ul-Jaded Campus. Our system is based on Cartesian coordinates. Depending on the type of problem under consideration, coordinate systems possessing special properties may allow particularly simple solution. In addition to locating the position of user it also locates and guides him towards the other locations.