For complex software systems, a central design concern is system architecture. The formal approach to architectural specification and refinement provides an effective way to ensure the correctness of those complex designs. In this chapter, we apply formal methods in the development process of a typical peer-to-peer system and demonstrate a stepwise paradigm for specifying, refining and implementing such kind of systems. The architectural considerations, formal specification, and possible refinement directions are discussed in details.