可抽查的产物（PCP 式思路）
这是"软化逻辑"里最出人意料的一个结果，这里把它借来当作设计原则。经典的证明检验要逐行读；概率可检验证明定理（PCP theorem）说明证明可以被"重写"成一种健壮的格式——在这种格式里，任何一处错误都会污染固定比例的位置——于是只检查 O(1) 个随机位置，就能以高概率抓到一个假证明。验证的成本之所以能骤降，不是因为检查者变聪明了，而是因为格式被强制成了会放大错误的格式。
这一手：约束产物本身，而不只是约束关口
对应到 harness 上：与其只在关口上加码（更多检查、更多预算），constitution 可以直接要求交付格式让错误变得响亮、不再局部：
- 贯穿代码的契约/断言——一处错误会违反附近的断言，使局部性在全局可见；
- 无处不在的类型——普遍的冗余意味着一个错误的值很难在每一条路径上都通过类型检查；
- 与主张交织在一起的测试；不变量表；流水线各阶段之间的校验和；
- 最古老的一个实例：复式记账——每笔交易都被写两遍，使损坏会打破一个看得见的余额。
原则是：在一种会放大错误的格式里，你藏不住错误。
经济账
这把成本从"验证者"（每个关口都要付一次，反复发生）移到了"格式"（一次性地在写作时付清）。在固定的 P×C 下，可达到的 α 会下降：便宜的随机抽查之所以能获得全局的覆盖力，是因为冗余会把错误带到你随便看向的任何一处。它同时反哺 gate-subsumption（冗余结构 = 各检查之间更多的静态蕴含关系）和 operationalizing-tolerances（抽查通过率是一个带有可计算 α 的可测量关口）。
harness 继承了这笔账：一个依赖格式级冗余的关口，单次调用更便宜，但要求执行者去维持这种冗余——维护断言、让测试保持同步、保住类型覆盖率。这不是免费的：这是提前欠下的 P×C 债务，只是会在未来所有的抽查上复利累积。
诚实的告诫
真正的 PCP 编码极不实用（多项式级的膨胀、代数编码）；harness 借的是"放大错误的冗余"这个原则，而不是那套构造本身。而且冗余本身也有代价：执行者必须去维护它（在写作时投入更多 P×C），过时的冗余（过期的注释/断言）反而是负面信号。所以冗余本身也需要 gate-subsumption 那套构建缓存失效的纪律。
这里还有一个陷阱：冗余可能制造出虚假的信心。如果断言太弱（只检查显而易见的性质），或者测试太稀疏（漏掉了边界情况），那么 harness 会报出很高的抽查通过率，而真实的 α 却仍然被隐藏着。格式确实放大了错误——但只放大了那些与冗余发生交互的错误。落在冗余覆盖范围之外的失效模式，是不可见的。
一句话
不要只顾着造更好的检查者——把产物逼进一种错误无处躲藏的格式，廉价的检查才会变得强大。