Paxos is a family of algorithms that solve consensus problems in unreliable distributed processor networks. Consensus is a process in which a group of participants in the system reach agreement on a result. As Paxos is widely used in large distributed systems, such as block chain system and Google file system, its security verification becomes more and more important. With Coq, a theorem proving tool, the formal description and definition of Lamport's basic Paxos algorithm are described, and it is proved that it satisfies the consensus property.