随着Internet的广泛应用和移动计算领域的不断扩大，人们对高可信软件的需求越来越多，从而对软件的可靠性和安全性提出了更高的挑战，因此软件安全问题再次显得至关重要。用形式化方法在软件开发过程中进行严格推理是提高软件安全性的根本途径。在众多的形式化方法中，近十年来从构造程序形式证明的角度来支持代码安全性的研究引起了广泛的关注。 按照对安全性质推理方法的不同，目前研究代码安全性主要有两类方法：基于类型论的方法、基于Hoare逻辑的方法。而后者正是本项目的研究领域。自动定理证明器和随之产生的出具证明的验证编译器都是这个领域的研究热点。相关的PCC项目和CAP项目具有重大的影响力。 本文的工作基于我们的现实验证汇编语言(RealisticCertifiedAssemblyLanguage，简称RCAL86)项目。它提出了一种低级的机器语言RCAL86和采用形式化方法构造证明的开发框架。本文介绍了基于构造形式证明的程序验证方法。该方法将形式化技术应用到程序验证领域，将Hoare逻辑的推理方式用于低级语言性质的推理。 本文重点讨论了程序满足安全性质的证明方法和技术，并且结合验证Buddy程序的构造过程详细讨论了验证程序的开发过程。文中对过程的三个阶段：标注、形式化、证明进行了重点阐述。文中不仅给出了每个阶段包含的内容，还根据构造验证Buddy程序的实践讨论了每个阶段遇到的主要问题、问题的解决方法以及总结了每个阶段工作的经验。本文还研究了采用证明工具Coq构造证明的方法、证明结构和证明策略等。Coq系统的使用简化了证明过程，提高了开发证明的效率。 验证Buddy程序的整个构造过程给出了开发程序形式证明的新思路。通过构造Buddy系统的验证程序，我们可以得知RCAL86语言具有很好的表现力，也可以得知基于构造形式证明的程序验证对于形式化方法的应用具有很好的借鉴价值。