当我审计 SystemVerilog 断言时，八个绿色形式证明变成了五个可归档证明
我亲眼看到一个合成形式验证看板报告了 8/8 PROVEN，随后又目睹其自身审计仅认证了 5/8 为 TRUSTWORTHY。这种逆转正是 Proof Firewall 的立论前提——这是我们针对 AI 生成的 SystemVerilog 断言（SVA）所构建的可运行治理演示系统，它改变了我希望绿色证明在进入流片签核评审前所必须达到的标准。
我在合成仲裁器、两级流水线和 CDC 跨时钟域上使用由测试夹具生成的「大模型生成」属性构建了该看板，因为令人不安的情况理应被清晰呈现。断言在属性清单中可能显得无懈可击，形式验证引擎也能返回绿色结果，然而该蕴含式可能从未真正起过检验作用，或者在相关设计行为已被破坏后依然持续通过。我此前一直将 PROVEN 这一字眼视作终点。构建这个演示系统迫使我将其视为证据审查的开端。
该 Proof Firewall 演示系统 在其默认路径中并不替代形式验证引擎、不接入真实 RTL，也不调用实时大模型。它被特意设计得更精简、更具可检查性：一个纯 Python 显式状态模型检查器负责评估合成迁移系统 IR，随后治理门控检查前件可达性、变异查杀以及影响锥（COI）。输出结果要么是归档已签名演示证书的理由，要么是将结果留存待人工评审的依据。
我最初陷入了对「绿标」的错误认知
我清楚地记得，该看板的最初版本之所以让人感到安心，正是因为它极为干净：八个属性、八个绿色徽章，以及让工作看起来已经大功告成的裸流程视图。我早期的本能是让演示系统更好地解释这一干净的结果。我曾以为工程任务在于呈现形式：展示证明、呈现断言，让仪表盘更容易被信任。绿色结果固然真实，但它回答的问题，远比评审人员需要提出的问题要狭隘得多。
随后，我让同样的八个属性接受了签核归档沟通真正要求的各项检查：前件是否曾经为真？如果修改设计的相关部分，断言是否会提出异议？它是否约束了有意义的 COI？这些问题远不如绿色徽章那般讨喜，因为它们拷问的是证明凭何立足，而不仅仅是求解器返回了什么。
我不得不放弃最初的构建思路。显示 8/8 PROVEN 的屏幕固然准确反映了裸流程基线，但作为签核依据而言却是不完整的。在经过防火墙审计后，同一个固定的合成看板得出了五个 TRUSTWORTHY 结果、一个 VACUOUS 结果和两个 WEAK 结果。其余三个结果并未被重新贴上成功的标签，而是连同解释其原因的证据一同被暂扣。证明标签与归档决策是截然不同的两种产物。
我在此处斟酌使用了「治理」一词。演示系统中的确定性检查使归档决策具备了可审查性。可选的 SVA 编写器可以提出断言，但模型检查器与策略门控决定最终裁决。智能体提供建议，代码做出裁决。 我试图让门控具有足够的清晰度，使得未通过的结果能发挥实际价值，而不仅仅令人尴尬。一个被暂扣的结果需要附带验证工程师能够检查、复现和质疑的明确理由。
ARB3 让人无法对该问题视而不见
我在 ARB3 中发现了最明确的失效，该合成仲裁器属性为 assert (g0 && g1) |-> (turn == 0)。在裸流程中，它显示为绿色。当我打开其波形与可达性证据时，前件 g0 && g1 在该合成仲裁器中实际上是不可达的。该蕴含式之所以被证明，仅仅是在狭义上因为它从未被迫对其所描述的状态承担检验责任。前件从未被触发。
当验证仪表盘上一片全绿时，这种区别说起来容易，却极易被忽视。我最初将该蕴含式理解为对仲裁行为的一项断言。可达性结果改变了我所看到的本质：这是一项触发条件从未发生过的断言。将其标记为 VACUOUS 远比保留绿色标签更有价值，因为它能引导评审人员查明是何种假设或激励导致了证明的空泛失效。
在制定策略标签时，我反复回顾这个面板。VACUOUS 听起来可能像是一个苛刻的结果，直到你考虑另一种情况：如果签核记录保留了一项证明，却未记录其前件从未触发，那么评审得到的就是一个失去了赋予其意义的先决条件的结论。更优的做法是让这种局限性显式化，并为人员留下具体可供质询的内容。该可达性记录理应与裁决结论并列存放。
我还必须克制将「空真」仅视为表面性警告的念头。如果该属性旨在约束某种仲裁条件，那么不可达的触发行为正是衡量该属性是否行使了预期行为的核心证据。仪表盘不应要求评审人员从绿色结果中去推测这一点，而应保留可达性发现，将该结果移出证书签发路径，并让下一步评审动作清晰明了。
行业背景进一步加深了我对这一问题严重性的认识。演示规范中引用的 2024 年 Wilson Research Group / Siemens EDA 研究报告显示，一次流片成功率仅为 14%。这并非 Veriprajna 的测算数据，这个合成看板也无意解释该数据。但这确实让我不再愿意将令人愉悦的仪表盘状态单独视为可靠证据。
流水线属性在我预期它应捕获的故障下依然得以幸存
我在测试 PIPE3 时遇到了第二个失效，这是一个合成两级流水线属性：assert v2 |-> (s2 == s2)。我当时想要一个简洁的断言示例，它读起来足够合乎逻辑，足以蒙混通过肤浅的审查。其后件是一个恒真式，它表达的是 s2 等于其自身。后件没有施加任何约束。
演示系统中的关键动作不仅仅是在文字上识别出恒真式。治理门控会注入相关的单点设计变异，并检查该属性是否能查杀它们。对于重点展示的弱流水线案例，PIPE3 记录了 0/6 的变异查杀结果。该属性在相关的损坏变体中依然幸存。这就是为什么策略分配了 WEAK，而不是允许原始的 PROVEN 结果作为归档证据生效。变异结果测试了有实际价值的敏感性。
在试图让这个例子显得不那么显而易见的过程中，我得出了一个令人不安的认知：人类读者可以看懂 s2 == s2 并迅速将其否决，但许多弱点并不会表现得如此直白。这就是为什么我不希望演示系统依赖操作人员去肉眼发现可疑字符串。真正有价值的产物是这一整套流程：可达性、相关的变异查杀测试、COI 以及记录其缘由的策略决策。
我逐渐将变异检查视为一种严谨拒绝轻率采信证明的方式。其目的不是制造戏剧性的失效，而是拷问该属性是否能察觉到其本应约束的行为中所发生的局部相关变化。当它无法察觉时，该结果向评审人员提供了切实可行的行动依据：在支撑签核记录之前，此断言需要强化或走不同的评审路径。
这也是为什么演示系统的基准测试需要明确界定其范围。在本地运行 python -m backend.bench 针对一组固定的已标注合成断言集得分 18/18，并识别出 6 个若在演示系统自身的无门控基线中会被直接盖章通过的证明。这些数据是对本演示系统已标注测试夹具的可复现性检验，而不是生产环境通过率，也并非针对大模型生成断言的普遍断言，更不是与商用形式验证工具的对比。
我不再试图让门控显得宽松
在最初的审计结果出来后，我面临一个设计选择：要么放宽暂扣裁决以使看板显得更加乐观，要么让看板拒绝认证其无法捍卫的内容。我选择了后者，因为真实的签核评审必须具备区分完整证明与有界证明、不可达前件与有意义属性、以及脆弱检查与能对相关故障行为作出响应的检查的能力。暂扣是一种评审结果，而非死胡同。
这种取舍体现在策略词汇表中。TRUSTWORTHY 可获得已签名的演示证书。BOUNDED-PROVEN、VACUOUS、WEAK、DEAD 以及 VIOLATED 则分别保留了暂扣该证书或升级上报结果的不同理由。例如在 CDC 测试夹具中，较强的属性 assert (req && !ack) |-> ##1 req 被判定为 VIOLATED，并生成了具体的合成反例波形。它说明了事务丢失或 CDC 失效类别，但这并不涉及客户芯片。
我并不认为这是在鼓吹取代验证团队现有的引擎。生产环境的方向是独立于具体引擎的：在现有形式验证工作流周围设置门控，并使其准入标准透明可查。在本演示中，真实引擎适配器与 RTL 接入被延后实现。演示所界定的边界是特意收窄的。 明确这一边界至关重要，因为它使论断与实际运行的系统保持相称。
如今我要求凭证与裁决结论并列
我一直在思考：当断言编写受到 AI 辅助时，签核会议真正需要何种产物？它不是来自编写者的置信度评分，而是一份记录——说明运行了哪些检查、可达性结果为何、查杀了哪些变异、COI 包含什么，以及策略为何允许或暂扣认证。评审需要的是可随时重新调取复查的证据。
这正是演示系统在 signoff_certificate.json 中导出的内容：逐个属性的裁决结论、可达性、变异结果、COI、适用时的反例记录以及一个 SHA-256 字段。我将证书构建为一份演示记录，因为评审人员应该能够在不盲目信赖绿色徽章的情况下重构决策过程。证书应当保留通往其裁决的完整路径。
如果你更愿意亲眼观看而不是读我的文字描述，这里是整个系统端到端运行的过程。
我将演示系统制作成可运行的，以便大家能够亲自检验 8/8 到 5/8 的逆转，而不是将其当作口号复述。我从中得出的结论虽然谦逊但经得起考验：值得归档的证明，必须附带其约束了什么、在何种破坏下幸存、以及他人为何可以信赖它的证据。绿标依然有用，它只是需要一份记录，让下一位评审人员能够判断它是否值得进入下一个环节。
