随着互联网的迅速发展和普及,网络数据流量越来愈庞大。企业信息化程度的不断加强,导致大量的数据亟待处理,数据已成为各类企业的命脉。传统的应用服务使用单一服务器模式,但是由于网络环境的不稳定,服务器容易发生数据丢失、节点宕机,严重影响了系统的可用性。在单机服务逐渐不能满足企业数据处理的需求情况下,人们开始搭建服务器集群的分布式系统。副本复制技术提高分布式系统的可靠性,在网络负载较大的情况下实现负载均衡,缓解服务器的压力。但是副本复制技术的引入,也带来了副本数据一致性等问题。为了保证系统的高可用性和一致性,就需要使用分布式一致性算法,Paxos算法便是其中非常重要的一类。共识问题是指分布式系统中一组参与者就一个结果达成一致的过程。Paxos能够很好的解决共识问题,越来越多的研究者将重点放在对算法本身的优化或者具体工程实现,Paxos在大型分布式系统得到了广泛的运用,比如区块链系统以及谷歌文件系统等。虽然Paxos的工程实现越来越多,但是关于算法安全性的形式化工作却很少,为了增强研究者和企业对Paxos的应用信息,其安全性证明越来越重要。所以,本文在定理证明工具Coq中形式化描述和定义了Lamport的Basic Paxos算法。Paxos是应用在非拜占庭容错模型下的基于异步通信网络的分布式一致性算法。消息可能会延迟、丢失、顺序错乱,系统节点可能会发生故障,也可以重启;但是系统中不会出现恶意节点。利用这些性质,我们设置全局消息通道来解决在异步网络中定义节点的发送与接收消息的困难;同时,Paxos的消息种类非常复杂,我们利用Coq类型检查机制完成了消息类型的统一;最后,因为Paxos算法流程涉及到系统节点的过往信息,为了避免函数递归出现栈溢出等异常情况,我们增加了这些过往信息字段的定义,并对其及时更新,以此解决了复杂计算问题。我们选取了任意系统时间点,证明了其满足共识性,从而完成了对Paxos的形式化验证。