区块链技术是当今正快速崛起的一门新兴技术,在数字金融、电子存证等关键敏感领域中具有强大的应用潜力,它在国家信息技术创新领域中占有重要地位,它已经被列入国家发展战略计划。在区块链技术中,最为关键的组成部分是智能合约,区块链系统中的重要资源与业务均由智能合约自动管理和完成。但由于区块链技术的新兴性和相关技术社区的快速发展,智能合约开发与使用过程中缺乏统一的约束与规范,存在安全隐患并面临可靠性风险,所以亟需相应的验证技术来保障智能合约的安全性与可靠性。针对上述问题,本文引入了高阶逻辑定理证明技术,并深入分析总结了高阶逻辑定理证明技术所存在的传统问题。同时,针对区块链智能合约在需求设计、实现和验证方面所面临的若干新的挑战,本文基于高阶逻辑定理证明技术提出了一套可用于保障区块链智能合约的安全性与可靠性的高效率、可扩展的模块化通用形式化验证框架。本文主要完成了以下五个方面的工作:（1）以归纳构造演算、柯利霍华德同构和匹配逻辑为基础,分析了在抽象逻辑系统中融合高阶逻辑定理证明技术和符号化执行,对柯利霍华德同构应用扩展的可行性,提出了一种与归纳构造演算逻辑环境深度嵌合的可扩展通用验证框架FSPVM,并可应用于区块链智能合约安全性与可靠性保障。（2）针对FSPVM蓝图形式化逻辑内存模块,详细分析了可执行语义在基于非Record抽象类型的形式化逻辑内存模型演算效率和基于记录抽象类型的形式化逻辑内存模型扩展性,提出了对应的解决优化方案,并基于多态抽象和模块化递归,构建了基于多级页表结构的形式化逻辑内存框架。（3）针对FSPVM蓝图源代码层级形式化规约语言模块,以及主流公链平台智能合约编程语言,构建了通用形式化规约语言Lolisa,在设计并实现Lolisa规约语言时,首次引入了广义抽象代数类型用于强化规约语言抽象语法树的类型系统,此规约语言作为EOS、Ethereum等主流公链平台智能合约编程语言子集,能支撑绝大多数情况下的智能合约建模,与此同时,还引入了语法糖层级隐藏形式化语法复杂规约,提高形式化模型的可读性。（4）针对FSPVM蓝图中的符号化执行引擎模块,详细分析了传统可执行操作语义建模过程中的演算与验证效率低下的问题,提出了对应的优化方案,通过实验对优化效果进行了验证;基于优化方案,实现了以Lolisa规约语言可执行形式化语义集为核心的符号化解释器,同时,设计并实现了配套的自动化验证策略库。（5）整个系统的核心模块的设计、建模、实现、属性定义与验证,均在Coq定理证明辅助器中完成,这就最大程度避免了因不同规范与实现方案所带来的语义鸿沟和自我正确性验证问题。在此,以验证实际智能合约代码为实例,整合上述工作得到了“一站式”区块链智能合的验证流程。当前,在区块链智能合约形式化验证领域中,仍然存在许多困难与挑战。本文旨在为验证各类型区块链智能合约代码安全性与可靠性方面提供新的理论依据和技术方法,希望为该领域的发展出一份力。