英文：Formal Verification 分类：science
用数学方法证明软件或硬件满足其规范的技术，杜绝"测试没覆盖"的漏洞。它把安全性建立在证明而非抽样之上，是安全关键系统的行业标准。
方法包括：模型检验（穷举状态空间，如 TLA+、SPIN）、定理证明（证明助手、SMT 求解）、符号执行与抽象解释；AI 的介入包括自动化不变量发现、证明搜索加速与反例分析。难点是形式化成本高，需要平衡验证深度与工程效率。
用于航天、汽车（ISO 26262）、区块链智能合约、操作系统与协议的正确性保障；大模型辅助形式化（如生成 Lean 证明、验证智能合约）正在降低门槛。
相关词条：AI 科学家 · AI for Science · AlphaFold · 数学定理证明 · 符号回归