形式化方法是计算机科学与软件工程领域的一套基于严格数学逻辑的技术与方法体系，核心目标是通过精确的数学语言、模型与证明手段，对软件 / 硬件系统进行描述、开发与验证，从根源上消除自然语言描述的歧义性，保障系统的正确性、可靠性与安全性。

普通软件开发 :以自然语言需求为起点，依靠经验、沟通、理解来设计编码。核心是 “实现功能”，优先保证可用、迭代快，依赖人工理解和经验把控逻辑。需求、设计、代码之间靠人脑翻译，存在理解偏差。

形式化方法开发 :以数学逻辑、严格规约为核心。先把需求转化为无歧义的数学模型 / 形式化规约，再基于模型开发。核心是证明正确性，从源头约束系统行为，追求逻辑严谨、零逻辑漏洞。

它广泛用于：

操作系统内核
编译器
芯片设计
航空航天
高铁信号系统
银行/密码学协议
区块链智能合约

普通开发 ：全程使用自然语言、流程图、UML 草图、口头沟通。

优点：通俗易懂、上手简单、沟通效率高；

缺点：语义模糊、存在二义性，不同人对同一份需求理解不一样。

形式化方法：使用形式化语言、数理逻辑、契约约束、数学公式（如 Z 语言、VDM、JML、OCL 等）。
优点：语法、语义严格定义，完全无歧义，所有人理解一致；
缺点：学习门槛高，可读性差，非专业人员难以看懂。

形式化方法的核心
1.形式化建模
先用数学语言描述系统。不是自然语言。因为自然语言有歧义。

2.形式化验证
证明：系统满足规格说明

3.自动推理
使用工具自动验证：

定理证明器
模型检查器
SAT Solver
SMT Solver