Mobile agent receives much attention recently in the distributed computing field. But the research on its formal model is immature. The necessity of the formal research of mobile agent is analyzed firstly. Then we introduce several representative formal models, analyze their drawbacks, and present the prospects for the future work.