---
title: "黑箱转向（四）：控制不可读之物，需要哪些证据"
url: https://lingming.blog/posts/2026/controlling-the-unreadable/
date: 2026-03-03
lastmod: 2026-08-31
tags: ["软件验证","软件测试","形式化方法","接口契约","AI 编程"]
categories: ["软件工程","计算机科学"]
description: "当实现无法被完整阅读，软件控制需要哪些证据？本文建立需求、契约、测试、实现分析与运行监控组成的五层保证体系。"
---

# 黑箱转向（四）：控制不可读之物，需要哪些证据


假设 AI 生成了一个转账函数，单元测试全部通过。我们能否据此放心上线？

还不能。测试可能只覆盖余额充足的正常路径，没有检查重复请求、并发扣款、货币精度、审计记录或下游超时。即使每一行代码都由人写，问题也一样存在。阅读能够发现某些错误，却无法穷尽输入、状态和环境；测试能够提供行为证据，也无法证明需求本身完整。

[上一篇]({{< relref "/posts/2026/the-collapse-of-linearity.md" >}})讨论团队理解与系统之间的认知债。本篇转向工程保证：当完整理解不可得时，怎样建立足够但不虚假的信心？

## 不是从“实现控制”切换到“约束控制”

接口契约、不变量、测试先行和形式验证都早于生成式 AI。它们不是黑箱时代突然出现的新方法，也没有取代实现检查。AI 改变的是相对成本：候选实现更容易产生，明确性质和核验证据便显得更稀缺。

因此，更准确的方向不是二选一，而是从单一证据转向**分层保证**：

> 说明我们主张系统满足什么，用相互独立的方法支持这项主张，并诚实记录仍未覆盖的条件。

这与安全关键领域中的 assurance case 思路相近。控制不是“测试绿了”的感觉，而是一条可以被质疑的主张—证据链。

## 第一层：先证明问题被定义

转账功能的第一层不是代码，而是业务和风险要求：

- 金额必须为正，并使用明确的货币与精度规则；
- 同一幂等键不能造成重复扣款；
- 未授权主体不能发起转账；
- 余额与账本必须保持一致；
- 下游超时不能留下无法判定的中间状态；
- 每次变更必须留下可审计记录。

这些要求包含功能、禁止行为和失败处理。若团队只给模型一句“实现转账 API”，生成器会用训练数据中的常见模式填补空白。实现可以整洁，却不一定符合这个组织的真实制度。

需求层的证据来自领域专家确认、威胁建模、历史事故、法规和用户场景。它的盲点是自然语言可能歧义，利益相关者也可能遗漏风险。

## 第二层：把关键性质写成契约和不变量

契约把部分要求变成更精确的边界：

- 前置条件：调用者已授权，金额与货币合法；
- 后置条件：成功时借贷双方账本变化守恒；
- 不变量：任何时刻总账不能因内部转账凭空增加或减少；
- 接口保证：重复幂等键返回同一业务结果。

类型系统、数据库约束、状态机和权限策略都可以承担这种工作。它们让一部分错误变得不可表达，或者在边界处立即失败。

但契约不会自动正确。若把“每天限额”写错，机器可以完美验证一个错误规则；若性质没有包含隐私泄漏，形式上的资金守恒也不能证明系统安全。约束减少行为空间，不替我们决定哪一个空间值得允许。

## 第三层：用多种测试探索性质

示例测试适合固定已知场景；性质测试从更广输入中寻找反例；状态机或模型测试适合检查操作序列；模糊测试可以探索解析器和协议边界；故障注入则检查依赖失败时的系统反应。

对于转账系统，可以让生成器产生不同金额、账户状态、重复请求和并发顺序，持续检验余额守恒与幂等性。QuickCheck 在 2000 年已经展示了用随机数据检验程序性质的方法，这并不是 AI 时代的新发明。

测试的力量在于找到具体反例，而不是证明“所有可能情况都没问题”。测试数据分布、模拟环境和断言质量都会限制结论。AI 可以帮助提出边界案例，也可能生成与实现共享同一误解的测试，因此高风险性质需要独立来源。

## 第四层：检查实现，而不是宣布实现无关

代码审查、静态分析、依赖扫描、动态分析和渗透测试仍然重要。行为测试可能发现“发生了错误”，实现分析更容易解释错误怎样发生，以及是否存在同类模式。

代码覆盖率在这里仍有用途：它能指出测试从未执行的语句或分支。它不能证明需求已经覆盖，也不能衡量断言质量。所谓“行为覆盖”如果不定义行为模型、输入分区和性质集合，就只是一个好听的新标签。

更合理的关系是：

- 需求覆盖问：重要主张是否有证据；
- 代码覆盖问：实现结构哪些区域从未执行；
- 性质测试问：给定生成分布是否找到反例；
- 变异测试问：测试是否能识别人为注入的错误；
- 静态分析问：是否存在某类结构性缺陷。

这些维度互补，没有一个可以单独取代其余部分。

## 第五层：用形式验证承担适合它的高风险主张

形式验证可以证明实现相对于形式化规格满足某些性质。seL4 微内核展示了机器检查的功能正确性证明能够达到很深层级，同时也明确列出编译器、硬件和规格等可信假设。

这正说明形式证明的边界：它证明的是模型中写出的性质，不是现实世界的一切正确性。完整验证成本高，也不必施加在每段低风险业务代码上。

更现实的做法是风险分配：

- 用类型和约束处理大量局部错误；
- 用模型检测检查有限状态协议；
- 用求解器验证关键权限与资源性质；
- 对安全内核、加密协议或高后果控制器投入更强证明；
- 对其余系统保留测试、审查和运行防护。

AI 可能帮助生成规格或证明，但规格与证明脚本仍需独立检查。由同一个模型同时提出实现、测试和“证明”，容易产生相关性失败。

## 第六层：上线以后仍需验证

前五层都无法完整复制生产环境。真实流量、数据分布、依赖故障和运维操作会暴露新的条件，因此保证必须延伸到运行期：

- 灰度或金丝雀发布限制初始影响；
- 指标、日志和追踪帮助识别越界；
- 对账和审计任务检查业务不变量；
- 限流、熔断与权限边界限制传播；
- 降级、前滚修复或回滚缩短影响时间；
- 事故复盘把新事实反馈到需求和测试。

运行监控不是承认前面的工程失败，而是承认开放系统总会遇到模型外事实。

## 把证据放进同一张表

| 层级 | 转账案例中的主张 | 主要证据 | 不能单独证明 |
| --- | --- | --- | --- |
| 需求 | 这是正确的业务与风险目标 | 领域评审、威胁模型 | 要求无遗漏 |
| 契约 | 关键状态必须守恒 | 类型、约束、不变量 | 契约符合现实意图 |
| 测试 | 代表性场景满足性质 | 示例、性质、故障注入 | 输入空间已经穷尽 |
| 实现 | 没有已知结构性缺陷 | 审查、静态与动态分析 | 所有行为正确 |
| 形式验证 | 指定模型满足指定性质 | 机器检查证明 | 模型外环境安全 |
| 运行验证 | 真实系统保持在边界内 | 监控、对账、灰度 | 未来不会出现新风险 |

这张表的价值不在于让流程变长，而在于防止证据越权。测试通过只能支持它实际检查的主张，代码可读也只能提高发现某些错误的机会。

## 结语：控制是可审查的信心

黑箱系统最危险的不是我们没有读过全部实现，而是我们无法说清自己凭什么相信它。

分层保证保留了理解的价值，也承认理解的边界。工程师可以阅读关键实现，同时用契约限制状态、用测试搜索反例、用形式方法证明高风险性质，并在运行期准备发现和恢复。

控制不可读之物，不是把内部过程忘掉，而是让每项重要主张拥有与其风险相称的证据。

## 延伸阅读与参考资料

- [Bertrand Meyer：Applying “Design by Contract”](https://doi.org/10.1109/2.161279)
- [Koen Claessen、John Hughes：QuickCheck](https://doi.org/10.1145/351240.351266)
- [Gerwin Klein 等：seL4 — Formal Verification of an Operating-System Kernel](https://doi.org/10.1145/1743546.1743574)
- [NIST：Recommended Minimum Standards for Vendor or Developer Verification of Software](https://www.nist.gov/itl/executive-order-14028-improving-nations-cybersecurity/software-supply-chain-security-guidance-0)
- [NIST：Secure Software Development Framework](https://csrc.nist.gov/pubs/sp/800/218/final)

*上一篇：[《黑箱转向（三）：认知债——团队知道得越来越少吗》]({{< relref "/posts/2026/the-collapse-of-linearity.md" >}})；下一篇：[《黑箱转向（五）：架构即风险几何》]({{< relref "/posts/2026/architecture-as-risk-geometry.md" >}})。*