Design of mobile agent systems requires tools and techniques appropriate to the task. Traditional models for distributed computing considers network to be static and considers failure of nodes as undesirable event. In the context of mobile computing these assumptions are no longer appropriate since nodes are not stable and can be switched off because of movements, or to save power. We argue that traditional model of distributed computing is no longer suitable for design and verification for mobile agent systems and therefore needs special attention. We studied the current trend in designing of such systems and tried to prove properties of an message delivery algorithm for mobile agent systems. We found that no formal model is adequate to prove the properties of mobile agent system in which we can explicitly reason about the location dependent behavior and fault tolerance. While trying to prove the properties of message delivery algorithm under some assumptions we found that model checkers were unable to do so because of state explosion problem while theorem provers were successful to some extent. We conclude by suggesting some options for exploring the same.