网络形式化验证这词，念出来就贵。扒掉壳其实没那么玄：一堆逻辑公式扔进 SMT 求解器，求解器把路由输入、故障场景穷举一遍，告诉你这网络会不会出事。
好看。但里面有一格，几乎没人愿意正眼瞧——那堆公式，是人手写的。
先画开看看。一个符号验证器，结构就三格：
┌──────────────┐
│ 符号编码 │ ← 人手写：这个协议怎么跑、这个 feature 什么语义
│ （逻辑公式） │
└──────┬───────┘
▼
┌───────────┐
│ 求解器 │ ← 穷举所有输入 / 故障组合
└─────┬─────┘
▼
会不会出事
下面两格是死的。求解器早就够用，穷举也不是瓶颈，买得起。问题全压在上面那格——它得把真实路由器的行为，一笔一笔翻译成逻辑公式。
填这格是什么感觉？每上一个新 feature，就得有人把它的行为拆开、写成公式、再拉真机对一遍。写错了也不会报错，它只会安安静静给你一个"安全"，而那个安全是假的。
这格为什么永远填不完？因为这个网络里压根没有一份官方答案。RFC 写得挺像规格，但它不是；厂商实现会偏离 RFC，这东西跨版本还会变。你照着 RFC 写出来的编码，撞上真机就是错的。
于是就出现一个很拧巴的局面：想验证的网络一大堆，真能上手验证的没几个。不是买不起求解器，是养不起那个控制面模型——写完还得一直写下去，谁维护谁知道。
两个月前（8 月 11 号）arXiv 挂了一篇，Self-evolving network verifiers，arXiv 2608.11340，Protogeros、Schneider、Vanbever 三个人，8 页 5 张图。通篇没讲怎么把求解器做得更强，讲的是怎么让那堆手写公式自己长大。想法粗暴得很：既然手写跟不上，那就别手写了。
它把路由器软件本身，当成唯一的、无歧义的规格来源。注意这句——不是 RFC，是跑起来的那玩意儿。然后套一个反例驱动的循环：
coding agent 提一个编码扩展
│
▼
┌───────────────┐
│ 符号编码 v_n │
└───────┬───────┘
│ 查一条具体路由
▼
跟 oracle 对一下 ← oracle = 仿真路由器，真值在这
│
┌─────┴─────┐
│一致 │不一致
▼ ▼
保留 这就是反例
│
▼
agent 照着这个 disagreement 改编码 ──┐
▲ │
└────────────────────────┘
等等等等，先别急。我第一版看这段的时候画错了。我以为它是让 agent 去"学协议"——好像 agent 得先把 OSPF areas 的语义搞明白，才能把编码写对。不是这个路子。
这套设计里，agent 不需要懂到能担保正确的程度。语义全压在 oracle 那边，它干的活只是缩小不一致。谁在背书"对"？是 oracle，不是模型。
初步证据是有的：他们让一个原型去教一个 3000 行的 SMT 验证器，三个它原本不支持的 feature——OSPF areas、BGP route reflection、L3VPN over EVPN。原型最后自己收敛到了跟 oracle 一致的模型上。
"初步"两个字别漏掉，这是原型不是成品，拿去说服你老板还早得很。但里面有一条我很喜欢：它自己摸出了厂商特定的行为。
这个点才让我咔哒一下扣上 💡
人手写编码的时候会发生什么？人会照着 RFC 写。撞上厂商偏差，第一反应是"实现有 bug"，要么就绕过去。厂商偏差在这套工作流里是噪音。
可这个循环把噪音当信号了——因为它唯一的裁判是仿真路由器，不是 RFC。谁跑得对，它就学谁。这两个东西的排序一换，整个味道就变了。
打个比方：这验证器像一台翻译机，把"网络会不会出事"翻成"一条逻辑公式成不成立"。翻得准不准，取决于词典。这篇论文说，别编词典了，让一个不会说这门语言的人，拿一台真机当标准答案，一句一句对，对不上就改词典。
这个比喻抓住的是"真值在外部、靠顶撞逼出来"这个方向。它漏风的地方在这：翻译机听起来是翻完就完了。不是。漏掉的那半句是——这台翻译机的词典每季度过期一次。你翻完，下个 release 出来，同一句话口音又变了，得重翻。所以它不是一个"翻好了"的状态，是一个一直在翻的状态。这是这篇东西最不舒服、也最老实的地方。
作者自己也没把话说圆。文里写，把模型生长自动化之后，主要挑战就从"建验证系统"挪到了"系统性地测试它"。我看到这句停了一下——这听着像解决，其实不是，是把问题往上游推了一层。
原来你怕的是"编码不准"，现在你怕的是"oracle 准不准"。仿真路由器是不是真机？如果不是，你学的就是仿真的行为，不是真机的行为。如果 oracle 自己偏了，agent 会一丝不苟、效率极高地把编码收敛到那个偏差上。它不怀疑裁判。
所以这篇真正留下的问题不是"能不能自动长"，是"你凭什么信那个 oracle"。他们提了个研究议程，就是围着这个转的——怎么信任、怎么用这种自动长出来的验证器。8 页纸 5 张图，摊下来就一个问题：自动化把人的活接走了，顺手把人的判断也接走了，判断那部分的替代品就是 oracle。它值不值得信，没人替你验。
照例留个自检：这个循环里，谁在定义"对"？要是你卡在"agent 到底懂不懂协议"，往回翻一格，那正是它不需要懂的地方。
下期画开哪个概念，你说了算。我候选清单上三个：embedding 为什么能"找相似"、KV cache 到底缓存了什么、还有"为什么大模型有时候会拒答"。
本期画开：验证器不卡在求解，卡在那张一直在变的地图。