你搭建了一个 n-version 系统。同一个关键函数的三个独立实现，一个选择多数结果的 voter，以及一种你已经规避了单点故障的满足感。
但你并没有证明这些函数是等价的。你只证明了它们能编译通过。
为什么等价性是 n-version programming 的隐藏基石
N-version programming 的核心思想是：如果某个实现存在 bug，其他实现大概率不会有，因此 voter 可以丢弃异常值。但这有个前提：输出必须是可比较的。
如果函数 A 返回 float，函数 B 返回 string，voter 根本无从判断。但即使类型匹配，语义差异也会带来致命问题。一个升序排列，一个降序排列。一个四舍五入，一个使用 banker’s rounding。voter 看到三个不同答案，却没有原则性的方法来选择。
关于 n-version programming 的文献中充满了研究表明：独立编写的程序往往以相关的方式失败。程序员会犯同样的错误。他们会误读同样模糊不清的规格说明。如果你的规格说明是”对这个列表排序”，一个程序员实现了 quicksort，另一个实现了 mergesort，你可能会认为它们是等价的。确实等价，直到你问起稳定性。或者直到输入中包含 NaN。
大多数团队跳过等价性检查，因为它看起来像是额外工作。事实并非如此。正是这项工作，让系统的其余部分变得有意义。
为什么你的测试套件只是在给你虚假的安全感
你写了 unit tests。两个函数都通过了。你宣布胜利。
这是一种范畴错误。Tests 只能证明 bug 的存在，永远无法证明 bug 的不存在。面对无限的输入空间，甚至只是很大的有限空间，你的 test coverage 不过是个舍入误差。两个函数在你想到的所有 case 上结果一致，却可能在凌晨 3 点生产环境里的那个关键 case 上分道扬镳。
我在一个包含两个 JSON parser 的项目中吃过这个苦头。一个用了 Python 内置的 json.loads，另一个为了性能手写了一个 parser。我们的 test suite 有五十个 case，两个都通过了。到了生产环境，一位客户发送了一个包含重复 key 的 JSON object。Python 的 parser 保留了最后一个值，我们手写的 parser 保留了第一个值。voter 看到两个不同的 object，直接 panic 了。
Property-based testing 更进一步。与其手工挑选输入，不如描述两个函数必须满足的属性，然后让 generator 去搜寻反例。下面是一个使用 Python Hypothesis 库的真实例子：
from hypothesis import given, strategies as st
import math
def round_half_up(n):
return math.floor(n + 0.5)
@given(st.floats(allow_nan=False, allow_infinity=False))
def test_rounding_equivalence(n):
assert round_half_up(n) == round(n)
if __name__ == "__main__":
test_rounding_equivalence()运行这段代码，Hypothesis 会迅速找到一个反例。round_half_up(2.5) 返回 3，而 Python 内置的 round(2.5) 返回 2，因为它使用的是 banker’s rounding，即舍入到最近的偶数。按某些标准，两个函数都是”正确”的。但它们并不等价。
Property-based testing 无法证明等价性。它能找到 unit tests 遗漏的 edge cases。这很有价值，但它仍然是证伪，不是验证。
SMT solvers 如何真正证明等价性
如果你想要一个证明，就必须离开 testing 的舒适区，进入 SMT solvers 的世界。思路很直接：将两个函数编码为逻辑公式，然后问 solver 是否存在某个输入会让它们产生不同结果。
对于有界域，这是机械化的操作。下面是一个使用 Z3 证明两个整数 max 实现等价的例子：
from z3 import Int, Solver, If, Abs
x = Int('x')
y = Int('y')
# Standard max implementation
max_standard = If(x > y, x, y)
# Algebraic max: (x + y + abs(x - y)) / 2
max_algebraic = (x + y + Abs(x - y)) / 2
solver = Solver()
solver.add(max_standard != max_algebraic)
result = solver.check()
print(result) # unsatZ3 返回 unsat，意味着不存在反例。在 Z3 的模型中，这两个函数对所有整数都是等价的。这是一个真正的证明，局限在 Z3 正在推理的理论范围内。
你也可以对更复杂的函数这样做。诀窍在于将函数表达为逻辑公式。对于 loops，你展开它们。对于 arrays，你使用 Z3 的 array theory。对于 floating point，你使用 Z3 的 FP theory，并接受 solver 在复杂表达式上可能 timeout 的事实。
“机械化”和”简单”之间的鸿沟，正是大多数团队卡住的地方。把一个 Python 函数翻译成 Z3 的语言，需要对两者都有深入理解。但一旦完成翻译，solver 就会承担繁重的计算工作。
没人愿意公开的权衡表
完整的 formal verification，为所有可能的输入（包括每一个 IEEE 754 edge case）证明等价性，是可行的。人们会为 cryptographic primitives 和 avionics systems 做这件事。它需要数周乃至数月的专家时间，以及 Coq 或 Isabelle 这样的工具。
Property-based testing 只需几分钟，能捕获真正的 bug，但不提供任何保证。
使用 SMT solvers 的 bounded verification 处于中间地带。它为一个定义明确的范围提供保证。这个范围可能覆盖 99.9% 的生产输入。这是否足够好，取决于失败的代价。
天下没有免费的午餐。选择与你风险承受能力和团队技术栈相匹配的工具。
懂得何时放弃的 voter
大多数 n-version 系统实现的是一个 naive majority voter：返回最常见的结果，如果没有多数则失败。一个更好的 voter 知道自己的无知。
from collections import Counter
def naive_voter(results):
if not results:
raise ValueError("No results to vote on")
counts = Counter(results)
winner, count = counts.most_common(1)[0]
if count > len(results) / 2:
return winner
raise ValueError("No majority found")
def informed_voter(results, input_sample=None):
if not results:
raise ValueError("No results to vote on")
distinct = set(results)
if len(distinct) == 1:
return results[0]
# Log disagreement for later analysis
if input_sample is not None:
print(f"Disagreement on input {input_sample}: {distinct}")
counts = Counter(results)
winner, count = counts.most_common(1)[0]
if count > len(results) / 2:
return winner
raise ValueError("No majority found")当 voter 发现特定输入类别上持续存在分歧时，这是一个信号。要么你的等价性假设是错的，要么你在某个实现中发现了一个 bug。两者都值得你知道。
voter 不只是用来选出获胜者的。它的存在是为了告诉你，你关于等价性的假设何时是错的。
接下来真正该做什么
从 property-based testing 开始。它成本低，能发现 bug，还能迫使你阐明”等价性”在你的领域意味着什么。是 bitwise 完全相同的输出？是在某个 epsilon 范围内的输出？还是满足相同 postcondition 的输出？
一旦精确定义了等价性，如果域是有限的且风险很高，就可以转向 bounded verification。使用 Z3、CBMC 或类似工具，为你的有界范围获得一个机械化的证明。
将完整的 formal verification 留给那些 bug 真的会出人命的部分。对于其他一切，了解你的证明的局限性，并在生产环境中监控分歧。最好的 n-version 系统，是知道自己不知道什么的系统。