1. 基础定义
形式化方法（Formal Methods）是计算机科学、软件工程领域一套以严格数理逻辑为底层基础的技术体系，用于对软件、硬件系统完成需求规约、设计建模、行为分析与正确性验证。
区别于日常模糊的自然语言需求描述，它使用集合论、命题 / 谓词逻辑、自动机、时序逻辑等数学符号体系，精确定义系统约束与运行规则，从根源消除文字歧义。
2. 三大核心分支
形式规约（Formal Specification）
使用专用形式语言（Z 语言、VDM、LTL 时序逻辑等）把系统需求转化为无歧义数学模型，明确输入输出、状态转换、安全约束。
形式推演与证明
基于数理逻辑推导证明系统满足关键属性（无死锁、数据安全、功能合规），分为人工交互式证明、自动化工具证明两类。
形式化验证
包含模型检测、定理证明两大主流技术，自动化遍历系统所有状态，找出逻辑漏洞、边界缺陷，广泛用于航空、芯片、操作系统等高可信场景。
3. 核心优势与局限
优势
精确无歧义：规避自然语言二义性带来的需求理解偏差；
可严格证明：唯一能从数学层面证明系统 “绝对正确” 的工程手段；
高危场景刚需：航天、自动驾驶、金融交易、芯片内核等不容出错的系统强制落地。
局限
学习门槛高：要求扎实离散数学、逻辑基础；
建模成本高：大型复杂系统完整形式化建模工作量巨大；
工具生态不完善：自动化验证工具上手难度大，普通业务开发很少全流程使用。
4. 典型应用场景
工业安全：航空机载软件、高铁信号控制系统；
底层基础软件：操作系统内核、编译器、密码算法库；
芯片设计：CPU、FPGA 硬件逻辑漏洞检测；
金融区块链：智能合约安全审计，杜绝重入、溢出漏洞。