Series C / Paper 04

計算機作為相對客觀認知載體：跨判定域驗證、信任鏈與異質錯誤通道

Computers as Relatively Objective Epistemic Carriers: Cross-Domain Verification, Trust Chains, and Heterogeneous Error Channels

版本：v0.1
日期：2026-08-14
狀態：Theory + executable counterexample paper

摘要

大型語言模型可以生成自然語言 claim、程式、資料分析、測試、形式化敘述與 proof artifact；但「模型生成了一個看似合理的結果」與「某個外部判定系統實際接受或執行了該 artifact」具有不同的認識論地位。本文提出 Relatively Objective Epistemic Carrier（相對客觀認知載體），用以描述程式執行器、編譯器、測試框架、reproducible build system、formal verifier、theorem prover 與獨立 proof checker 在 AI 研究閉環中的角色。

本文中的「相對客觀」不表示計算機完備、不出錯或等於真理。相反地，本文將計算驗證明確建模為條件信任鏈：

\text{world claim} \rightarrow \text{formalization/specification} \rightarrow \text{artifact} \rightarrow \text{compiler/interpreter} \rightarrow \text{runtime} \rightarrow \text{verifier} \rightarrow \text{certificate}.

若 specification fidelity、verifier soundness、semantic preservation、runtime/environment assumptions 均成立，則 machine acceptance 可被提升為對原 claim 的條件性支持；若其中任一關鍵邊界失效，machine acceptance 不再保證 world-level correctness。

本文證明四個基礎結果。

第一，Conditional Carrier Soundness：若每個 translation / execution / verification link 都 sound，則 carrier acceptance 對原 claim sound。

第二，Trust-Boundary Union Bound：若 false certificate 只能在至少一個信任邊界失效時發生，則 false-certificate event 的機率被各 boundary failure probability 的 union bound 所控制。

第三，Reproducibility Orthogonality：deterministic reproducibility 只能證明固定 artifact 在固定 capture 條件下可重放，不能單獨推出 artifact 符合正確 specification；因此錯誤程式可以穩定、精確而可重現地產生錯誤答案。

第四，Heterogeneous Carrier Suppression：在 false-accept events 條件獨立時，多個異質 carrier 同時錯誤接受 false claim 的機率乘法下降；但若存在 common-mode failure，該收益會被共同失效機率形成下限。

公開技術系統提供了這一理論的現實對照。Lean 以小型 trusted kernel 檢查 core terms，並提供 independent checker / comparator 路徑以進一步降低單一實作錯誤的風險；CompCert 將 compiler passes 的 semantic preservation 機器化證明；Nix reproducible-build infrastructure 把 dependency 與 sandbox 納入重建條件；AlphaEvolve、AgentForge 與 Agentic Verifier 則將程式執行與 automated evaluation 直接放入 AI 的生成—驗證閉環。

同時，反例同樣重要。Lean 官方在 2026 年 7 月的 4.32.1 與 4.32.2 point releases 分別修正 kernel soundness bugs，直接證明「formal checker」本身仍有 implementation-level trust boundary。VeriAct 的 2026 研究又顯示，大量 verifier-accepted formal specifications 可能實際上錯誤或不完整，說明 verifier pass 不等於 specification fidelity。

因此本文的核心命題是：

\boxed{ \text{Computer verification does not create absolute truth; it moves a claim into a different, inspectable, replayable, and often less-correlated error channel.} }

這種跨錯誤通道轉譯，正是多 AI 自主研究閉環能夠降低單純語言幻覺風險的主要機制之一。

關鍵詞： epistemic carrier；formal verification；execution feedback；reproducibility；trusted computing base；specification gap；semantic preservation；AI agents；cross-domain verification

1. 問題：為什麼「跑過」和「說過」不一樣？

令 Agent：

A_i

產生自然語言 claim：

c.

如果另一個 Agent 只閱讀 $c$ 再回答：

\text{agree / disagree},

兩者仍可能共享：

相同語言模型偏差；
相同 retrieval error；
相同錯誤 premise；
相同自然語言歧義。

若 Agent 反而生成一個 artifact：

a

並將其送入執行器：

E(a,x;\eta)=o,

其中：

$x$ 是輸入；
$\eta$ 是執行環境；
$o$ 是實際 output；

則系統得到一項不同型態的 evidence。

一旦 $a$ 、 $x$ 與 $\eta$ 固定，執行 output 不再由「哪一個 Agent 比較有說服力」直接決定。

這是本文稱計算機為相對客觀載體的第一個意義。

2. 定義：Epistemic Carrier

定義 1：認知載體

令原始 claim space 為：

\mathcal C.

一個 epistemic carrier 定義為：

\mathfrak C = ( \Sigma, \tau, \mathcal A, \mathcal E, V, \mathcal T ),

其中：

$\Sigma$ ：carrier 可判定的 specification language；
$\tau:\mathcal C\rightarrow\Sigma$ ：claim translation / formalization；
$\mathcal A$ ：artifacts；
$\mathcal E$ ：execution / evaluation semantics；
$V$ ：verification operator；
$\mathcal T$ ：trusted assumptions / trusted computing base。

carrier 不必是 theorem prover。

它可以是：

unit test；
compiler；
interpreter；
database query；
numerical solver；
simulation；
formal checker；
proof assistant；
independent verifier；
reproducible-build infrastructure；
physical sensor interface。

3. 相對客觀性

定義 2：Source-Conditional Objectivity

令 artifact $a$ 已固定，來源 Agent identity 為：

I\in\{A_1,\ldots,A_N\}.

若 carrier output 滿足：

P( O \mid a,x,\eta,I=A_i ) = P( O \mid a,x,\eta,I=A_j )

對所有 $i,j$ 成立，則稱該 carrier 對固定 artifact 具有 source-conditional objectivity。

在 deterministic setting：

O = E(a,x;\eta),

此條件退化為：

O \perp I \mid (a,x,\eta).

這並不表示：

O = \text{truth}.

它只表示：

\boxed{ \text{同一個 artifact 的 carrier result 不再由來源 Agent 的語言權威直接決定。} }

4. 認知轉譯階梯

本文區分至少七個層級。

L0. Linguistic Claim

c.

只有自然語言敘述。

L1. Executable Artifact

c \rightarrow a.

claim 被轉成程式、query 或其他 machine-readable artifact。

L2. Executed Claim

(a,x,\eta) \rightarrow o.

artifact 被真正執行。

L3. Tested Claim

存在 test suite：

T=\{t_1,\ldots,t_m\}

且：

a\models T.

L4. Reproducible Claim

獨立或重建環境得到相同 artifact / output：

R_1(a,x) = R_2(a,x).

L5. Formally Checked Claim

存在 formal specification：

\sigma

與 verifier：

V(a,\sigma)=\mathrm{accept}.

L6. Independently Cross-Checked Claim

多個具有不同 implementation lineage 的 checker：

V_1,\ldots,V_k

共同接受。

L7. World-Grounded Claim

formal specification 本身另有理由被認為忠實表達原始 world claim：

\mathrm{Faithful}(c,\sigma).

核心順序為：

\boxed{ \text{linguistic} \rightarrow \text{executable} \rightarrow \text{reproducible} \rightarrow \text{formally checked} \rightarrow \text{world-grounded}. }

但這不是保證每一層必然比前一層更真。

它只是逐步增加不同種類的可檢查結構。

5. Trust Chain

令原始命題為：

\phi.

其 formal specification：

\sigma=\tau(\phi).

令 artifact 為：

a.

要把：

V(a,\sigma)=\mathrm{accept}

提升成：

\phi

的支持，需要多個 link。

A1. Specification Fidelity

\mathrm{Sem}(a)\models\sigma \Rightarrow \phi.

或者更強：

\phi \iff \sigma.

A2. Verifier Soundness

V(a,\sigma)=\mathrm{accept} \Rightarrow \mathrm{Sem}_{\mathrm{src}}(a)\models\sigma.

A3. Compilation / Translation Preservation

若 artifact 經編譯：

a \rightarrow a',

則要求：

\mathrm{Sem}_{\mathrm{src}}(a) \sim \mathrm{Sem}_{\mathrm{exec}}(a').

A4. Runtime Fidelity

實際執行必須符合被驗證的 machine semantics：

\mathrm{Exec}(a',x;\eta) \in \mathrm{Sem}_{\mathrm{exec}}(a').

A5. Environment Assumptions

相關 dependency、configuration、numerical mode、input data、hardware 與 sandbox assumptions 沒有破壞前述語義。

因此完整鏈條為：

\boxed{ \phi \leftarrow \sigma \leftarrow a \leftarrow \mathrm{compiler} \leftarrow \mathrm{runtime} \leftarrow \eta. }

6. 定理 1：Conditional Carrier Soundness

定理

若 A1–A5 全部成立，且：

V(a,\sigma)=\mathrm{accept},

則：

\phi

成立。

證明

由 A2：

V(a,\sigma)=\mathrm{accept} \Rightarrow \mathrm{Sem}_{\mathrm{src}}(a)\models\sigma.

由 A3 與 A4，source-level verified behavior 被保留到實際 execution semantics。

由 A5，實際環境滿足上述 preservation 所需 assumptions。

因此實際 artifact behavior 滿足：

\sigma.

由 A1：

\sigma \Rightarrow \phi.

故：

\phi.

證畢。

解讀

這個結果不是：

\boxed{ \text{computer says yes} \Rightarrow \text{absolute truth}. }

而是：

\boxed{ \text{computer says yes} + \text{trust-chain assumptions} \Rightarrow \text{conditional guarantee}. }

7. CompCert：Semantic Preservation 作為中間鏈條

CompCert 的核心意義不是「C 程式因此絕對正確」。

它證明的是 compiler translation 的一個特定關係。

若 source program：

S

滿足一組 acceptable behaviors：

\Sigma,

且 CompCert 將：

S \rightarrow C,

則編譯後 code $C$ 保留被證明的 source-level property。

這對本文非常重要。

因為它顯示：

\boxed{ \text{formal verification can close one trust boundary without pretending to close all trust boundaries.} }

若 source-level specification 本身錯誤：

\Sigma\neq\Sigma^\star,

CompCert 的 semantic preservation 不會神奇地修正它。

8. Lean：Small Kernel 與 Independent Checkers

Lean 的 architecture 提供另一個典型例子。

高階 tactics、elaborator 與 automation 可以非常複雜，但最終新增到 environment 的 core definitions / proof terms 由較小的 trusted kernel 檢查。

因此：

\text{tactic bug} \nRightarrow \text{proof soundness failure}

只要錯誤結果無法通過 kernel。

更高風險情況下，Lean 官方文件進一步建議使用：

sandboxed build；
comparator；
exported proof representation；
official kernel；
independently implemented external checker。

這是：

\boxed{ \text{TCB minimization} + \text{implementation diversity}. }

但它仍不是 absolute truth。

Lean 官方明確列出 remaining assumptions，包括：

Lean logic 本身的 soundness；
comparator plumbing；
sandbox security；
不存在同時影響所有 checkers 的共同 bug；
theorem statement 沒有人為或表示層誤導。

9. Formal Checker 也不是絕對 Oracle

這一點在 2026 年變得尤其清楚。

Lean 4.32.1 的官方 release notes 修正一個 kernel soundness bug。

Lean 4.32.2 又修正另一個 kernel soundness bug；後者甚至可在某些情況下影響 comparator 路徑，而 independent checker nanoda 不受同一 kernel bug 影響。

因此：

\boxed{ \text{formal verification} \neq \text{implementation infallibility}. }

更精確地：

\boxed{ \text{formal guarantee} = \text{theorem} + \text{logic} + \text{proof object} + \text{checker implementation} + \text{trusted boundary}. }

這不削弱 formal methods 的價值。

恰好相反，它說明為什麼：

small kernel；
independent implementation；
exported proof object；
reproducible checking；

會實質增加 epistemic strength。

10. Specification Gap

Verifier 回答的問題通常是：

artifact 是否滿足 specification？

而不是：

specification 是否正確描述使用者真正想問的世界？

令 intended specification 為：

\sigma^\star.

實際提交給 verifier 的 specification 為：

\tilde\sigma.

即使：

V(a,\tilde\sigma)=\mathrm{accept},

也可能：

\tilde\sigma\neq\sigma^\star.

因此：

\boxed{ \text{verification success} \nRightarrow \text{specification fidelity}. }

VeriAct 的 2026 結果正直接針對此問題：研究發現一大批 verifier-accepted specifications 實際上錯誤或不完整，可能 over-constrain 或 under-constrain inputs / outputs，而普通 verifier pass 無法發現。

所以本文將 specification fidelity 放在 trust chain 的第一層，而不是最後才補一句 limitation。

11. 命題 2：Reproducibility Orthogonality

命題

存在 artifact $a$ 與錯誤 specification relation，使得：

R_1(a,x)=R_2(a,x)=\cdots=R_k(a,x)=o

對所有重放環境成立，但：

o

仍不滿足 intended world-level claim。

證明

取一個 deterministic but wrong program 即可。

例如 intended function：

f(x)=x^2.

實作：

\tilde f(x) = \begin{cases} x^2,&x\geq0,\\ -x,&x<0. \end{cases}

對：

x=-2,

有：

\tilde f(-2)=2,

但：

f(-2)=4.

若所有重放環境 deterministic 地執行同一 $\tilde f$ ，則每次都得到：

2.

因此結果完全 reproducible，但仍然錯誤。

證畢。

所以：

\boxed{ \text{reproducibility} \perp \text{semantic correctness} }

在邏輯上不能互相推出。

12. Reproducible Builds 的真正認知價值

Nix 的 reproducible-build model 特別清楚地顯示這個區分。

若獨立 infrastructure 從同一 source 與 dependencies 得到 bit-for-bit identical artifact，這會增加：

\boxed{ \text{artifact provenance confidence}. }

它有助於檢查：

build infrastructure 是否偷偷修改輸出；
source 與 binary 是否一致；
dependency closure 是否可重建。

但 Nix 自身文件也指出：

repeated build 兩次並不能證明 reproducibility；
timestamps 與其他 nondeterminism 仍可能洩漏進 build。

更重要的是，即使 binary 完全 reproducible，也不能推出：

\boxed{ \text{the program implements the right idea}. }

因此 reproducibility 解的是：

\text{provenance / reconstruction problem},

不是完整的：

\text{world-truth problem}.

13. Execution Grounding

對 LLM Agent 而言，execution 的主要價值是把：

\text{predicted behavior}

轉成：

\text{observed machine behavior}.

AlphaEvolve 將候選程式交給 automated evaluator 實際 verify、run 與 score。

AgentForge 將 sandboxed execution 設為 code change 傳播前的 mandatory verification。

Agentic Verifier 則主動搜尋高區分度的 test inputs，以實際 execution 找出 candidate programs 的 behavioral discrepancy。

共同結構都是：

\boxed{ \text{generate} \rightarrow \text{execute} \rightarrow \text{observe} \rightarrow \text{revise}. }

這正是 Series C 所說 autonomous research closure 的基礎回授。

14. 定理 3：Trust-Boundary Union Bound

令：

F_1,\ldots,F_m

為 trust chain 中不同 failure events。

假設：

\{ V=\mathrm{accept} \land \neg\phi \} \subseteq \bigcup_{j=1}^{m}F_j.

亦即：若 carrier 錯誤接受 false claim，至少有一個 trust boundary 必須失效。

若：

P(F_j)\leq q_j,

則：

P( V=\mathrm{accept} \land \neg\phi ) \leq \sum_{j=1}^{m}q_j.

證明

由 event inclusion：

P( V=\mathrm{accept} \land \neg\phi ) \leq P\left( \bigcup_jF_j \right).

再由 union bound：

P\left( \bigcup_jF_j \right) \leq \sum_jP(F_j) \leq \sum_jq_j.

證畢。

意義

增加一個 formal verifier 並不是把：

q=0.

而是把原本模糊的：

\text{LLM may be wrong}

拆成一組更可定位的 failure surfaces：

\boxed{ \text{specification} + \text{translation} + \text{checker} + \text{compiler} + \text{runtime} + \text{environment}. }

這就是「認知載體」的工程價值。

15. 異質錯誤通道

假設 false claim：

\neg\phi

被 $k$ 個 carriers 檢查。

第 $i$ 個 carrier false accept event：

F_i.

若：

P(F_i\mid\neg\phi)\leq q_i

且條件獨立，則：

P( F_1\cap\cdots\cap F_k \mid \neg\phi ) \leq \prod_{i=1}^{k}q_i.

因此：

\boxed{ \text{heterogeneous independent carriers} }

有機會產生乘法式錯誤抑制。

例如：

LLM reasoning；
Python execution；
symbolic algebra；
Lean checker；
independent external checker；
empirical dataset；

若 failure ancestry 足夠不同，聯合 evidence 比「再叫同一模型想一次」更強。

16. Common-Mode Failure

但 carriers 也可能共享共同失效。

令：

C

為 common-mode failure event，且：

P(C\mid\neg\phi)=q_c.

在：

\neg C

條件下，剩餘 carrier failures 獨立，機率為 $q_i$ 。

則：

P( \text{all accept} \mid \neg\phi ) \leq q_c + (1-q_c) \prod_iq_i.

當：

q_c

很大時，即使：

k\rightarrow\infty,

也有：

P( \text{all false accept} \mid \neg\phi ) \gtrsim q_c.

因此：

\boxed{ \text{carrier count} \neq \text{carrier independence}. }

典型 common-mode failure 包括：

所有 tools 依賴同一錯誤 dataset；
所有 verifiers 使用同一錯誤 specification；
多個 checkers 共享同一核心 bug；
所有 simulations 使用同一錯誤 physical model；
多個 Agents 直接複製同一上游 claim。

17. Relative Objectivity Index

本文不宣稱存在唯一客觀性 scalar，但可定義工程型指標。

令：

$R$ ：replayability；
$P$ ：provenance completeness；
$I$ ：implementation independence；
$S$ ：specification fidelity evidence；
$T$ ：trusted-base compactness；
$G$ ：external grounding。

定義：

\mathrm{ROI} = w_RR + w_PP + w_II + w_SS + w_TT + w_GG.

其中：

w_j\geq0, \qquad \sum_jw_j=1.

這不是 universal truth metric。

它只是一個工程排序：

哪一個 evidence carrier 更容易被重放、追溯、交叉檢查與獨立審計？

18. Epistemic Carrier Certificate

一項 machine-grounded claim 不應只保存：

\text{output}.

本文建議最小 certificate：

\boxed{ \chi = ( c, \sigma, a, x, o, \eta, V, h_a, h_\eta, p, t ) }

其中：

$c$ ：原始 claim；
$\sigma$ ：formal / executable specification；
$a$ ：artifact；
$x$ ：input；
$o$ ：output；
$\eta$ ：environment；
$V$ ：verifier；
$h_a$ ：artifact hash；
$h_\eta$ ：environment / dependency fingerprint；
$p$ ：provenance；
$t$ ：timestamp。

若有 independent checker：

V_1,V_2,\ldots,V_k,

也應一起寫入 certificate。

19. 與 Paper 03 的 Admissible Worlds 接合

Paper 03 定義：

\mathcal A_t

為目前仍被 evidence 允許的 world set。

一個 carrier certificate：

\chi

應被轉成 constraint：

K_\chi \subseteq \Omega.

若 $\chi$ 的 trust chain 尚未完整，系統不應直接使用：

\mathcal A_{t+1} = \mathcal A_t\cap K_\chi

做 hard contraction。

而可採 weighted / provisional constraint：

K_\chi^{(\omega)}.

只有當：

provenance 足夠；
verifier 被信任；
specification fidelity 有外部支持；
common-mode risk 可接受；

才升級為較強 world elimination。

因此：

\boxed{ \text{machine result} \rightarrow \text{epistemic certificate} \rightarrow \text{admissible-world update}. }

20. 計算機為何特別適合作為 AI 的外部載體？

不是因為計算機無錯。

而是因為它具有幾項 LLM 自然語言輸出不總是具有的性質：

20.1 Determinate Interface

明確 input / output。

20.2 Replayability

相同 artifact 可以重跑。

20.3 Inspectable State

程式碼、logs、diff、test result 可以保存。

20.4 Executable Counterexample

一個 failing input 可以直接推翻某些 behavioral claim。

20.5 Independent Implementation

同一 proof object 可以交給不同 checker。

20.6 Formal Semantics

部分 domain 可以明確定義：

\text{what counts as correct}.

因此計算機是：

\boxed{ \textbf{high verification-density epistemic substrate}. }

而不是：

\boxed{ \textbf{complete epistemic substrate}. }

21. 失敗模式

21.1 Wrong Specification

V(a,\tilde\sigma)=\mathrm{accept}

但：

\tilde\sigma\neq\sigma^\star.

21.2 Test Overfitting

a\models T

但存在：

x^\star\notin T

使：

a(x^\star)

錯誤。

21.3 Reproducibly Wrong

每次 execution 都一致，但一致地錯。

21.4 Checker Bug

formal kernel 或 verifier implementation 存在 soundness bug。

21.5 Compiler / Runtime Mismatch

被證明的 source semantics 與實際執行 artifact 不一致。

21.6 Numerical / Environment Drift

dependency、floating semantics、random seed、hardware 或 configuration 改變結果。

21.7 Shared Grounding Failure

不同 carriers 最終都依賴同一錯誤 source 或 assumption。

21.8 Malicious Artifact

artifact 可能利用 verifier、build process 或 sandbox vulnerability。

22. 本篇可執行 Counterexample Checker

本文附帶一個純 Python structural checker。

它不冒充 Lean 或 formal proof assistant。

它檢查四件事。

22.1 Test Pass 不等於 Specification Correctness

intended function：

f(x)=x^2.

buggy implementation：

\tilde f(x) = \begin{cases} x^2,&x\geq0,\\ -x,&x<0. \end{cases}

若 test suite 只有：

\{0,1,2,3\},

則全部通過。

但：

x=-2

時：

\tilde f(-2)=2\neq4.

22.2 Reproducibly Wrong

對：

x=-2,

重跑多次永遠得到：

2.

因此：

\text{reproducible}=1

但：

\text{correct}=0.

22.3 Wrong Specification Can Be Verified

若錯誤 specification 只要求：

\tilde f(x)\geq0,

buggy implementation 在有限檢查 domain 上完全通過。

但它仍不滿足 intended specification：

\tilde f(x)=x^2.

22.4 Heterogeneous Carrier Bound

取：

q_1=0.1, \quad q_2=0.05, \quad q_3=0.02.

若獨立：

q_{\mathrm{all}} = 0.1\times0.05\times0.02 = 0.0001.

若存在：

q_c=0.1

common-mode failure，則：

q_{\mathrm{all}} \leq 0.1 + 0.9\times0.0001 = 0.10009.

直接顯示：

\boxed{ \text{heterogeneity helps only when failure correlation is actually reduced}. }

23. 與自主研究閉環的關係

一個只有語言生成的系統：

\text{hypothesis} \rightarrow \text{paper}.

較弱。

加入 carrier：

\text{hypothesis} \rightarrow \text{code} \rightarrow \text{execution} \rightarrow \text{data} \rightarrow \text{verification} \rightarrow \text{revision}

後，系統開始把自己的 claim 投射到不同判定域。

因此 AI 自主研究真正重要的能力不只是：

\boxed{ \text{generate new claims}. }

而是：

\boxed{ \text{manufacture new evidence channels for its own claims}. }

這是從 LLM 到 autonomous research system 的關鍵轉變之一。

24. 結論

本文提出「計算機作為相對客觀認知載體」的條件理論。

「相對客觀」不表示：

計算機完備；
formal methods 絕不出錯；
verifier pass 等於 world truth；
reproducibility 等於 correctness。

它表示：

\boxed{ O \perp I_{\mathrm{source}} \mid (a,x,\eta) }

以及 machine carrier 可以提供：

固定接口；
重放；
provenance；
executable counterexample；
independent checker；
formal semantics。

完整可信度仍依賴：

\boxed{ \text{specification fidelity} + \text{verifier soundness} + \text{semantic preservation} + \text{runtime fidelity} + \text{environment assumptions}. }

因此本文最重要的結論不是：

\text{Computer} = \text{Truth}.

而是：

\boxed{ \textbf{Computer} = \textbf{a relatively objective, conditionally trusted, high-verification-density epistemic carrier}. }

對 AI 系統而言，真正重要的認知躍遷是：

\boxed{ \text{claim} \rightarrow \text{artifact} \rightarrow \text{execution} \rightarrow \text{certificate} \rightarrow \text{cross-carrier comparison}. }

下一篇將正式把這些元件組成一個最小自主研究閉環：

Series C / Paper 05 — Minimal Closure Conditions for Autonomous Research.

參考文獻

Lean FRO. The Lean Language Reference: Elaboration and Compilation — The Kernel. Current documentation, accessed 2026-08-14.
Lean FRO. Validating a Lean Proof. Current documentation, accessed 2026-08-14.
Lean FRO. Lean 4.32.1 Release Notes. 2026-07-22.
Lean FRO. Lean 4.32.2 Release Notes. 2026-07-28.
Leroy, X. et al. The CompCert C Verified Compiler / CompCert project documentation and semantic-preservation proofs. Current CompCert 3.17 documentation, 2026.
NixOS. Reproducible Builds. Current project documentation.
Google DeepMind. AlphaEvolve: A Gemini-powered coding agent for designing advanced algorithms. 2025.
Misu, M. R. H., Ma, I., & Lopes, C. V. VeriAct: Beyond Verifiability — Agentic Synthesis of Correct and Complete Formal Specifications. arXiv:2604.00280, 2026.
Kumar, R. et al. AgentForge: Execution-Grounded Multi-Agent LLM Framework for Autonomous Software Engineering. arXiv:2604.13120, 2026.
Ma, Z. et al. Scaling Agentic Verifier for Competitive Coding. arXiv:2602.04254, 2026.
OpenProver: Agentic and Interactive Theorem Proving with Lean 4. arXiv:2607.09217, 2026.

狀態標記

Definitions: Epistemic Carrier、Source-Conditional Objectivity、Trust Chain、Relative Objectivity Index、Carrier Certificate。
Proved: Conditional Carrier Soundness、Reproducibility Orthogonality、Trust-Boundary Union Bound、Heterogeneous Carrier Suppression under independence。
External technical grounding: Lean kernel / external checker model、CompCert semantic preservation、Nix reproducibility、AlphaEvolve execution evaluation、VeriAct specification-gap result、AgentForge / Agentic Verifier execution grounding。
Counterexamples: wrong specification、test overfitting、reproducibly wrong artifact、formal-checker implementation bug、common-mode failure。
Not claimed: computer completeness、absolute machine objectivity、formal verification infallibility、verifier acceptance implies world truth without specification fidelity。