闭合验证回路

AI agents 产出软件的速度，已经超过任何团队验证软件的速度。工程的瓶颈由「写出代码」转移到了「相信写出的代码」。

这并非第一次发生。早期程序员曾抗拒 compiler，因为他们往往真能写出更好的 assembly。Compiler 最终赢得信任，不只因为快，而是因为它翻译的语言具有精确语义：程序员定义程序做什么，compiler 决定如何实现。自动化只有与验证同行，才能真正取代手工劳动。

AI agent 的输入却是开放的自然语言，有时甚至来自不可信来源；输出则会直接成为可运行代码。它比 compiler 更自由，也更难验证。Datadog 的回答是 harness-first engineering：不把逐行阅读 agent 代码当作正确性的主要来源，而是先建设一套能在数秒内自动证伪的验证装置。

Agent 生成代码，harness 验证代码，production telemetry 校验现实；一旦出错，反馈就更新 harness，agent 再尝试一次。

这个 harness 可以由 deterministic simulation testing（DST）、形式化规范、shadow evaluation 与 observability feedback loop 组成。具体严谨程度不同，原则一致：让验证快速、自动，把人类无法扩展的审查工作交给机器。Datadog 早期的 BitsEvolve 已验证这条路径：只要 correctness oracle 足够紧，LLM 就能自由探索；再强的模型与更多人工 review，也无法补偿一个松散的 harness。

01 / REDIS-RUST从遗漏中，一层层学会验证

redis-rust 是第一次让单个 coding agent（Claude Code + Opus 4.5）构建完整系统。数小时内，它就围绕 actor-per-shard 与 CRDT 产出了可编译、可测试的 Redis-compatible server。但「测试通过」掩盖了细微错误：错误消息偏离 Redis 语义，抽象被过度设计，许多时间相关路径根本没有被触及。

团队没有用更多 review 堵漏洞，而是把每次漏网之鱼变成下一层验证。首先加入与真实 executor 并行的 HashMap shadow-state oracle，逐操作比较响应；它能抓基本语义，却看不见 timing-dependent bug，于是再加入带 fault injection 的 DST。

DST 需要可检查的 invariant，于是 replication 与 gossip protocol 被写成 TLA+ specification；CRDT merge property 用 Rust 工具 Kani 做 bounded proof；系统级正确性由 Maelstrom + Knossos 在 1、3、5 个节点上检查 linearizability；最后补上官方 Redis Tcl compatibility suite。

让真实流量成为裁判

形式化与模拟之后，团队用内部缓存系统 Ephemera 做 empirical verification：让 redis-rust shadow cluster 与 Redis 8.4 接收同一份 workload。初始 latency 相当，但内存竟高出 8 倍——代码为 exhaustive micro-benchmark 硬编码预分配了 512 × 8KB buffer。

metrics 把问题变成 agent 可优化的目标。数分钟内，agent 提出并实现三项优化，将 memory footprint 降低 87%。这就是闭环的雏形：不是凭感觉改快，而是由真实 workload 反馈、由指标决定去留。

02 / HELIX把 Harness 提升为系统工程

Helix 是构建在 object storage 上的 Kafka-like streaming service。吸收 redis-rust 的教训后，团队采用多 agent 协作，工作流也改成 constraint-first：design artifact 就是 contract，系统语义必须明确，每件 artifact 都接入能将错误证伪的反馈机制。

Raft、WAL、tiering、DST、service layer 与 Kafka wire protocol 分别设计，但 agent 无权自行发明系统含义：什么数据算 durable、何时算 acknowledged？什么算 committed、什么对 consumer visible？每个 failure boundary 上 crash 会发生什么？这些问题必须先变成 invariant，再允许实现向前推进。

DST：五秒一次的反馈回路

DST 抽象物理时间，使执行确定化，并在 network、disk 与 node 层人工注入故障。团队再用 BUGGIFY 扩大并发操作互相干扰的窗口，结合 metamorphic、roundtrip（如 decompress(compress(bytes)) == bytes）和 differential testing，让每个约 5 秒的 seed 都跑真实 production code。

它曾捕捉到一个 WAL bug：in-memory truncation 发生在 on-disk sync 之前；当注入 disk fault 时，segment 永远不会重试，最终数据丢失。修复方式是 copy-on-write。模拟把错误精确指到现场后，答案很明显；但单元测试发现不了，code review 也只能碰运气。

# deterministic failure → reproducible repair
seed 48172 → disk fault after memory truncation
invariant: acknowledged ⇒ durable
result: replay exact sequence, fix with copy-on-write

每个组件先跑绿 500 个 seeds，再扩到跨组件 1000 万 seeds，最后进入系统级 Kafka semantics：每条 acknowledged message 都必须可消费，consumer offset 必须单调递增，leadership change 不得丢 write。

性能优化：有安全网的 hill-climbing

正确性锁定后，优化变成受控搜索：agent 提方案，完整 DST suite 通过后再测 throughput；失败即撤回。Helix 从 zero-copy handler 和消除 contention 起步，随后走向 Raft pipelining、buffered WAL。actor architecture 的转向由人类批准，一天后性能达到 fio 测得峰值磁盘吞吐的约 93%，同时仍通过全部 DST。

在 staging 中，单个三节点 Raft group 每秒承载约 10,000 条 APM profiling 消息。其 producer p50 latency 为 22.2ms，基线 Kafka cluster 则是 116ms。人类的角色很窄却关键：定义系统与 invariants、加强 DST harness、设置可测目标、批准架构改变；设计草案、实现、修复与优化主要由 agent 对着 harness 完成。

03 / SCALABILITY INVERSION验证的经济学倒转了

过去 code review 最易扩展：每个团队都已经在做。formal verification 最难扩展：昂贵、专业，通常只用于 failure 后果极重且寿命很长的 safety-critical system。Coding agents 改变了成本曲线——LLM 能生成 TLA+、编写 DST harness、运行 Kani proof，把昔日数月的投资压缩成自动 pipeline stage。

Review 没有消失，但专业能力从检查每颗铆钉，转移到了设计 load test。团队不再把时间耗在追赶 agent 的每一份 diff，而是用于收紧 invariant、扩大 simulation coverage、连接 telemetry feedback loop。新增一条 invariant，可以在未来每次迭代中捕获一整类 bug；一次 review 通常只能服务眼前的 diff。

有了 harness，code review 变成一层 bloom filter：它是快速闸门，而不再是正确性的来源。Reviewer 阅读的不是 diff，而是 harness 输出——更像阅读 EXPLAIN ANALYZE，而不是阅读代码。

包括 redis-rust、Helix 与一些达到 300,000 行代码的实验在内，人类仍在闭环里：设计 harness、设目标、批架构；agents 则持续对验证结果迭代。规模化的关键不再是「有多少人能 review」，而是「有多少系统属性可被自动验证」。

04 / VERIFICATION FRONTIER可委派的边界，就是可验证的边界

任何能通过 tests、proofs、simulations 或 measurements 自动验证的 property，都可以把更多责任委派给 agent；无法验证的部分，人类必须留在 loop 中。这条边界就是 verification frontier。

但如果 harness 本身错了呢？不完整的 invariant 会制造虚假信心。此时 observability 负责闭合最后一环：production metrics、logs、traces 与 trajectories 把真实执行反馈进验证 pipeline，暴露模型世界与现实世界的偏差，再反过来修订 harness。

Formal methods 的价值不只在工具，而在于把 constraint 表述得精确、machine-checkable、unambiguous。Property tests、deployment shadow evaluation、production telemetry，都是 invariant reasoning 在不同高度的投影。建议并不复杂：按 failure 的代价，成比例投资 harness。