你建了一個 n-version 系統。同一個關鍵函式的三份獨立實作、一個選出多數結果的 voter，以及一種自己已經搞定單點故障的溫暖感覺。

你並沒有證明這些函式是等價的。你只證明了它們編譯得過。

為什麼等價性是 n-version programming 的隱形基礎

N-version programming 的概念是：如果其中一個實作有 bug，其他的大概不會有，所以 voter 可以丟掉異常值。這假設了輸出是可以比較的。

如果函式 A 回傳 float，函式 B 回傳 string，那 voter 根本無從判斷。但即使型別一致，語義差異也會害死你。一個升冪排序，一個降冪排序。一個四捨五入，一個銀行進位法。voter 看到三個不同答案，卻沒有任何原則可以決定該選哪個。

n-version programming 的文獻裡充滿了研究，顯示獨立撰寫的程式經常以相關的方式失效。程式設計師會犯同樣的錯誤。他們會誤讀同一份模糊的規格。如果你的規格是「排序這個清單」，一位程式設計師實作了 quicksort，另一位實作了 mergesort，你可能會假設它們是等價的。的確是，直到你問起穩定性。或者直到輸入包含了 NaN。

大多數團隊跳過等價檢查，因為感覺像額外工作。它不是。它是讓整個系統其餘部分變得有意義的工作。

為什麼你的測試套件只會給你虛假的信心

你寫了單元測試。兩個函式都通過。你宣布勝利。

這是類別錯誤。測試只能證明 bug 存在，永遠不能證明 bug 不存在。面對無限的輸入空間，甚至只是很大的有限空間，你的測試覆蓋率只是個捨入誤差。兩個函式可以在你想到的每個案例上意見一致，卻在凌晨三點生產環境中真正重要的那個案例上分道揚鑣。

我在一個有兩個 JSON parser 的專案上硬吃了這個教訓。一個用了 Python 內建的 json.loads，另一個為了效能用手刻的 parser。我們的測試套件有五十個案例。兩個都通過。在生產環境中，有位客戶送來了一個有重複鍵的 JSON 物件。Python 的 parser 保留了最後一個值。我們手刻的 parser 保留了第一個。voter 看到兩個不同的物件就當機了。

Property-based testing 比較接近。與其手工挑選輸入，你描述兩個函式必須滿足的性質，然後讓產生器去尋找反例。這裡有個用 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 無法證明等價。它會找到你的單元測試漏掉的邊界案例。這很有價值，但它仍然是證偽，不是驗證。

SMT solver 如何真正證明等價

如果你想要證明，就得離開測試的舒適圈，進入 SMT solver 的世界。概念很直接。把兩個函式編碼成邏輯公式，然後問 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)  # unsat

Z3 回傳 unsat，代表不存在反例。這兩個函式在 Z3 模型中的所有整數上都是等價的。這是真正的證明，受限於 Z3 正在推理的理論。

你也可以對更複雜的函式這樣做。訣竅在於把你的函式表達成邏輯公式。迴圈就展開它們。陣列就用 Z3 的 array theory。浮點數就用 Z3 的 FP theory，並接受 solver 在複雜表達式上可能會 timeout。

「機械化」和「簡單」之間的鴻溝，就是大多數團隊卡住的地方。把 Python 函式翻譯成 Z3 的語言需要同時理解兩者。但一旦翻譯完成，solver 就會做掉苦工。

沒人想公開的權衡表

完整的形式化驗證——為所有可能的輸入（包括每個 IEEE 754 邊界案例）證明等價——是可行的。人們會為密碼學原語和航空電子系統這樣做。它要花上數週或數月的專家時間，而且需要 Coq 或 Isabelle 之類的工具。

Property-based testing 花幾分鐘就能找到真正的 bug，但不提供任何保證。

用 SMT solver 進行有界驗證則位於中間。它為一個定義明確的範圍提供保證。那個範圍可能涵蓋了你 99.9% 的生產輸入。這夠不夠好，取決於失效的代價是多少。

天下沒有白吃的午餐。選一個符合你風險承受度和團隊專長的工具。

知道何時該放棄的 voter

大多數 n-version 系統實作了一個天真的多數 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，還會逼你具體說出「等價」對你的領域來說到底是什麼意思。是位元級完全相同的輸出？在某個 epsilon 範圍內的輸出？滿足相同後置條件的輸出？

一旦精確定義了等價，如果領域是有限的且風險很高，就進入有界驗證。用 Z3、CBMC 或類似工具，為你的有界範圍取得機械化證明。

把完整的形式化驗證保留給那些 bug 真的會害死人的部分。其他的一切，都要知道你的證明有其極限，並在生產環境中監控分歧。最好的 n-version 系統，是知道自己不知道什麼的系統。