2026-10-22 06:00:00
本文永久链接 – https://tonybai.com/2026/10/22/go-concurrency-concurrent-ml-events
大家好,我是Tony Bai。
【导读】
Go 把 CSP 带进了千家万户,channel 和 select 几乎成了并发的代名词。但有开发者最近指出:1990 年代的 Concurrent ML(CML)在 CSP 之上又往前走了一步,只做了一件事——把“通信操作”从一条语句变成一个值。就是这个小小的变化,让“组合、封装、取消”这些在 Go 里要靠 context 和约定硬撑的事,变得顺理成章,还顺手解决了 goroutine 泄漏。这个老模型,Go 能学到什么?
【文章要点】
select 是语法,不是值:通信的“描述”和“执行”被绑死,无法封装、无法组合。sync 才触发执行;select、超时、取消都是同一个抽象。handle-evt(提交后动作)、choice-evt(选择)、guard-evt(提交前准备)。context 约定层层传递。goroutineleak profile 是同一思路的“检测版”,而非“回收版”。
写过 Go 的人,大概都对这段代码不陌生:
select {
case ch1 <- 5:
case y := <-ch2:
default:
}
select 很强:多个通信操作里,只有一个会被选中,其余原封不动。但原文《ConcurrentML: Improving on Go’s concurrency model》的作者 Nikhil 指出了一个容易被忽略的事实:
在
select里,ch1 <- 5是一段“动作描述”;一旦把它拿出来,它立刻变成“执行”。
也就是说,在 Go 里:
通信的“描述”和“执行”,被 Go 语法绑死在了一起。这正是 CML 要拆开的地方。
CML(Concurrent ML)诞生于 1990 年代中期,出自 John Reppy 等人之手。它的关键思想只有一句话:把通信操作提升为一个“值”(称为事件,event),执行则交给 sync。
今天对这套思想支持最完整的语言是 Racket。对照一下:
| 目的 | Go | Racket(CML) |
|---|---|---|
| 立即发送 | ch <- 5 |
(channel-put ch 5) |
| 描述“发送” | 无法脱离 select | (channel-put-evt ch 5) |
| 描述“接收” | 无法脱离 select | channel 本身就是事件 |
| 执行 | 语句到达即执行 | (sync evt) |
注意,channel-put-evt 不会发送任何东西,它只返回一个值。只有被 sync 时,才真正尝试通信。事实上,阻塞式的 channel-put 本身就能用事件定义:
(define (channel-put ch val)
(sync (channel-put-evt ch val)))

事件是值,意味着它能做所有值能做的事:赋给变量、当返回值、放进 struct、被各种“组合子”继续加工。
handle-evt:提交后的动作(post-commitment)你可以把 select 的每个 case 理解成一个“提交点”:选中它,其余作废。case 后面的语句,就是提交之后的动作。CML 把这部分挂在事件本身上:
(sync
(handle-evt (channel-put-evt out-ch x) (λ (_) (loop y (+ x y))))
(handle-evt quit-ch (λ (_) (displayln "quit"))))
choice-evt:“选择”本身也是个事件Go 里“选择”只能写在 select 中;CML 里“选择”也是值,可以被封装、返回、再组合。Nikhil 给的例子是:
(define (fetch-from-fastest-url url1 url2)
(choice-evt (http-get-evt url1)
(http-get-evt url2)))
; 谁先返回用谁,并叠加 5 毫秒的超时
(sync (fetch-from-fastest-url url1 url2)
(timeout-evt 5))
注:上面代码中的
http-get-evt在原文中是示意 API,并非标准库函数。
关键在于:在 sync 之前,真正的请求根本没有发出去。库作者只负责“二选一”,调用者再决定要不要加超时,双方互不迁就。而 Go 里,“起两个 goroutine 各自返回 channel”和这件事不是一回事:goroutine 一被启动就开始干活了。
guard-evt:提交前的准备(setup)与 handle-evt 对偶,guard-evt 接受一个“制造函数”,在 sync 真正开始时才执行,并用它返回的事件顶替自己。比如打印服务里“每次请求新建一个响应 channel”这类准备动作,就可以收进事件内部,调用者完全无感。
这个话题其实并不新。2016 年,Guile 的维护者 Andy Wingo 在博客上发过一篇《concurrent ml versus go》,当时他的结论是:Go 的 channel + select 和 CML 表达力基本相当。他还特意邀请读者“来纠错”。
纠错很快就来了。第二天,他在《is go an acceptable cml?》里承认:自己错了,并给出了一个经典例子。
假设有一个“把数字加 1”的转换器,在 Go 中通常这么写:
func onePlus(in <-chan int) <-chan int {
out := make(chan int)
go func() { out <- 1 + <-in }()
return out
}
然后给它套一个超时:
select {
case v := <-onePlus(numbers):
fmt.Println(v)
case <-time.After(0):
fmt.Println("timeout")
}
如果超时先触发会怎样?onePlus 里的 goroutine 依然在等 numbers,将来某个时刻它可能取走一个数字,然后卡在 out <- ... 上,永远没人接收。结果是:一个数字凭空消失,还白白泄漏了一个 goroutine。
而在 CML 里,转换是用 handle-evt 挂在事件上的:
(sync (handle-evt numbers add1)
(timeout-evt 0))
只有当 numbers 这个分支真的被选中时,消息才会被取走并加 1,否则什么都不会发生。
Go 里当然也能改写成 case msg := <-ch: return msg + 1,但 Wingo 指出,这把“加 1”和“超时”两个关注点搅在了一起。表达力的差距,就在于能不能把转换封装在事件内部。
故事还有后续。Wingo 也发现,CML 其实可以建在“类 Go”的运行时之上——读者 Vesa Karvonen 就给出了基于 Clojure core.async 的 CML 概念验证实现。但 Michael Sperber 提醒他:把非 channel 事件包装成 goroutine + channel,性能开销可能高达 10 倍(Wingo 在文中转述了这一数字)。所以更合理的方向或许是:让 channel 的收发建在事件之上,而不是反过来。
公允起见,当年评论区也有人指出,Go 其实有
reflect.Select可以在运行时动态构造 select。但它解决的是“分支数量动态”,依然没有解决“描述可以脱离 select 独立存在”的问题。
Go 的取消(cancel)靠 context.Context:约定每个函数接收 ctx,监听 Done(),调用者用 WithTimeout / WithCancel 控制。它有效,但全靠约定,且 ctx 必须穿透整条调用链。
CML 的做法是:取消也是一种事件,叫 nack(negative acknowledgement,否定确认)。通过 nack-guard-evt,制造函数会拿到一个特殊的 nack-evt,它有三种结局:

放到 Nikhil 的“打印服务”例子里,效果是这样的:
(define (print-evt service msg)
(nack-guard-evt
(λ (nack-evt)
(define resp-ch (make-channel))
(thread (λ ()
(sync nack-evt
(channel-put-evt (print-service-print-ch service)
(print-req msg resp-ch nack-evt)))))
resp-ch)))
nack-evt 知道,不会卡在回复上。
最值得注意的一点是:print-evt 的 API 完全没变。调用者不需要知道有取消逻辑,更不需要额外的 Context 参数。Nikhil 也坦言,这部分是 CML 与 Go 最接近的地方——本质上都是“监听一个事件来感知取消”,区别只是:Go 把它放在顶层并逐层传递,CML 则让事件自己决定是否参与取消。
Go 最让人头疼的陷阱之一:goroutine 一旦阻塞在永远不会就绪的操作上,就会连同它引用的内存一起泄漏。
CML 的运行时语义很干脆:
如果一个线程只阻塞在某些事件上,而线程和这些事件都不再被其他存活的对象引用,那么它可以被垃圾回收。
所以 Racket 代码里,随手 thread 一个“可能永远等不到的发送”完全没问题——没人关心它,GC 自然会收走。原书《Concurrent Programming in ML》把这种“先投机地派生线程去发送,哪怕不会被接受”的写法,称为一项重要的 CML 编程技巧。
Go 这边也在朝这个方向走。查阅 Go 1.27 发布说明:
goroutineleak,位于 runtime/pprof,也可通过 net/http/pprof 的 /debug/pprof/goroutineleak 端点访问;一个最简单的例子:
func leak() {
ch := make(chan int)
go func() { ch <- 1 }() // 没人接收,ch 也无处可达
}
你可以在程序运行一段时间后,用下面的方式导出报告:
pprof.Lookup("goroutineleak").WriteTo(os.Stdout, 1)
这里要特别分清:Go 1.27 是“发现并报告”泄漏,而 CML 是“直接回收”不可达的阻塞线程。前者是诊断工具,后者是语言语义。Nikhil 也提到,相关提案和论文都没有提及“这个能力在 CML 生态里早已存在”,说明知道这段历史的人并不多。
先泼点冷水:
但对日常写 Go 的人,至少有四条可以马上用上的启发:
select 里加个超时,就把转换逻辑也混进去;把“转换”和“等待”分开设计。ctx 或 done channel 是惯例,但别忘了要有人负责关闭它们。goroutineleak:很多线上缓慢增长的内存,可能就是这类泄漏。CML 的思想可以浓缩为一句话:把通信操作表示为独立于执行的值。
由此,选择、取消、前置准备、后置处理,都统一在“事件”这一个抽象下;再加上“阻塞线程可被 GC”,并发代码才真正做到了“便宜到可以随便用”。
你可能永远不会在生产环境中用 Racket,但这个 30 年前的模型,值得每个 Go 开发者花一个下午读一读——不是为了替代 Go,而是为了看清:你习以为常的 select,其实只是一个更大设计空间里的点。
资料链接:
声明:本文案例代码以原文及相关资料为基础,部分 Go 代码为示意,实际使用前建议本地运行验证。
还在为写 Agent 框架频频死循环、上下文爆炸而束手无策?我的新专栏 《从0 开始构建 Agent Harness》 将带你:
扫描下方二维码,开启从 0 开始构建Agent Harness 的实战之旅。

你的Go技能,是否也卡在了“熟练”到“精通”的瓶颈期?
继《Go语言第一课》后,我的《Go语言进阶课》终于在极客时间与大家见面了!
我的全新极客时间专栏 《Tony Bai·Go语言进阶课》就是为这样的你量身打造!30+讲硬核内容,带你夯实语法认知,提升设计思维,锻造工程实践能力,更有实战项目串讲。
目标只有一个:助你完成从“Go熟练工”到“Go专家”的蜕变! 现在就加入,让你的Go技能再上一个新台阶!

商务合作方式:撰稿、出书、培训、在线课程、合伙创业、咨询、广告合作。如有需求,请扫描下方公众号二维码,与我私信联系。

2026-10-21 06:00:00
本文永久链接 – https://tonybai.com/2026/10/21/go-htmx-templ-sqlc-fullstack-gophercon-uk-2026
大家好,我是Tony Bai。
【导读】
一个后端工程师,被前端的状态管理折磨到烂尾了一个副业项目。直到他换上 Go + HTMX + templ + sqlc,终于把它做完了。这场 GopherCon UK 2026 的演讲,没有堆砌概念,只讲真实踩坑:HTMX 怎么用、HTML 为什么比 JSON 更适合做 Web 接口、什么场景千万别用它。
【文章要点】
hx-trigger 防抖搜索、页面加载后懒加载、OOB 多区域更新、响应头控制、HX-Redirect。
2021 年,Haseeb Majid 想做一个多人派对游戏 Banter Bus。玩法类似 Jackbox:大家输入房间码进入同一个房间,一起玩。
后端用 WebSocket 维护状态、防作弊,他驾轻就熟。前端用 Svelte,一开始还行,后来越写越乱:store、全局状态、各种同步,最后彻底失控。
他是后端工程师,对前端没有太多热情,也就没有动力专门去学“最佳实践”。结果就是:项目搁浅,成了副业项目坟场里的又一个名字。
转机出现在 2023 至 2024 年。他读到 HTMX 团队的文章,决定再试一次。这一次,项目真的做完了。
在 GopherCon UK 2026 上,他把这套方案拆开讲了一遍。演讲的案例是他自己的园艺记录应用 Let’s Go(用来记录那些被他养死的植物)。
一句话:HTMX 是一个约 50KB(压缩后)的小库,让你用 HTML 属性直接向后端发请求。
流程只有四步:

没有 JSON 序列化,没有前端状态管理,也没有手写 fetch。
最小示例:植物时间线的“添加事件”表单,只需要两个属性。
<form hx-post="/plants/1/events" hx-target="#timeline">
<input name="event_type" placeholder="浇水 / 换盆 / 施肥" />
<textarea name="notes"></textarea>
<button type="submit">记录</button>
</form>
<div id="timeline"><!-- 服务端返回的 HTML 会替换这里 --></div>
hx-post:提交时向该地址发 POST。hx-target:把返回的 HTML 放到哪里。不写 hx-target 时,默认更新的是发起请求的元素本身。
传统 SPA 的老毛病:前端存一份状态,后端存一份状态,两边不同步,你开始排查“到底谁错了”。
HTMX 的做法是:前端只是一个“哑”界面,告诉后端“该显示什么”,后端说了算。
对 Banter Bus 这类多人游戏尤其关键:状态必须在服务端,否则玩家改个请求就能给自己加一百万分。
HTMX 就是一个 JS 文件,你可以:
go:embed 打进 Go 二进制。不需要 npm,不需要 package.json。想追踪更新,也可以交给 Renovate 这类依赖机器人提 PR。
演讲者回应了最常见的质疑:“LLM 写 React 很强,为什么还要折腾 HTMX?”
他的答案很朴素:
LLM 写出的 Go 代码,我能判断好不好;LLM 写出的 React 代码,我只能看它“能跑就行”。
再加上 HTMX 的数据流非常直白:这个请求发到哪个端点,返回什么 HTML,一眼看完,没有分散在前端各处的状态。人容易审查,LLM 也容易理解。
<input type="search" name="q"
hx-get="/plants"
hx-trigger="input changed delay:300ms"
hx-target="#plant-list"
hx-push-url="true" />
hx-trigger:输入变化后延迟 300 毫秒再请求,相当于防抖;hx-push-url:把查询参数写进浏览器地址栏,搜索结果可以直接分享。对比同样功能的 Svelte 实现,要自己声明变量、监听参数变化、写 fetch、维护列表。当然,这不是严格的同口径比较,但复杂度差异一目了然。
时间线要跑一堆昂贵的 SQL?让页面先出来:
<div hx-get="/plants/1/timeline" hx-trigger="load">
加载中...
</div>
页面加载完成后,HTMX 自动请求,并用返回结果替换占位内容。
更新植物健康度,同时要刷新多个组件,还要弹出提示。难道要返回整页?
用 hx-swap-oob(Out of Band)即可:服务端返回几段带 ID 的 HTML,HTMX 按 ID 找到页面上的对应位置分别替换。
<!-- 服务端返回的片段 -->
<span id="health-badge" hx-swap-oob="true">健康度:良好</span>
<div id="toast" hx-swap-oob="true">已更新</div>
后端也能“指挥”HTMX:
HX-Retarget:忽略前端设置的目标,改去更新别处,比如错误提示;HX-Reswap:改写替换策略。注意一个细节:HTMX 的默认替换策略是 innerHTML,只替换目标元素的内部内容;想连元素本身一起替换,使用 outerHTML。另外,HTMX 默认不会替换 4xx、5xx 响应的内容,要展示错误提示,需要返回 200 或调整响应处理配置。
这是演讲者踩过的坑:普通 302 重定向在 HTMX 请求里不会跳转,登录页会被整个塞进原来那个小表单里。
解决办法:识别 HX-Request 请求头,改用 HX-Redirect。
func redirect(w http.ResponseWriter, r *http.Request, url string) {
if r.Header.Get("HX-Request") == "true" {
w.Header().Set("HX-Redirect", url)
w.WriteHeader(http.StatusOK)
return
}
http.Redirect(w, r, url, http.StatusSeeOther)
}
删除前的二次确认,没必要请求服务器。演讲者推荐用 Alpine.js 处理这类局部状态:
<div x-data="{ open: false }">
<button @click="open = true">删除植物</button>
<div x-show="open">
<p>确定删除吗?</p>
<button hx-delete="/plants/1">确认</button>
<button @click="open = false">取消</button>
</div>
</div>
他也给出了警告:别把 JavaScript 写成字符串塞进属性里。编辑器不识别,高亮失效,可读性更差,“两头的坏处都占了”。判断标准很简单:当你自己都看不懂这些属性时,就老老实实写几行 JS。
整体架构仍然是 Go 圈熟悉的三层:

templ 是专为 Go 设计的模板工具,特别适合 HTMX 这种“返回局部 HTML”的场景。它的杀手锏是:完全类型化,并自带语言服务器(LSP),编辑器里有补全、跳转、类型报错。
package components
templ Timeline(entries []db.TimelineEntry) {
<div id="timeline">
for _, e := range entries {
@EntryCard(e)
}
</div>
}
写完 .templ 文件后,执行 templ generate 生成 Go 代码(文件头带有“请勿编辑”提示)。类型不对,生成时就报错,而不是等到运行时。
Handler 里使用它非常自然:
func (h *Handler) AddEvent(w http.ResponseWriter, r *http.Request) {
entries, err := h.svc.AddEvent(r.Context(), r.PathValue("id"), r.FormValue("event_type"), r.FormValue("notes"))
if err != nil {
http.Error(w, "服务异常", http.StatusInternalServerError)
return
}
components.Timeline(entries).Render(r.Context(), w)
}
templ 还支持布局:定义带 { children... } 的基础模板,页头页脚只改一处。
有观众追问:标准库
html/template不行吗?演讲者的回答很坦诚:标准库也可以,可以先从简单做起,嫌烦再引入 templ,毕竟它是新增的一个依赖。他选 templ,主要因为类型检查和 LSP 体验。
-- name: ListTimeline :many
SELECT id, plant_id, event_type, notes, created_at
FROM timeline_entries
WHERE plant_id = $1
ORDER BY created_at DESC;
执行 sqlc generate,就得到强类型的结构体和查询方法。
它的价值在于没有魔法:SQL 是你自己写(或让 LLM 写)的,一眼能审查,不会冒出一百行莫名其妙的 ORM 拼接 JOIN。
这是 HTMX 最常被追问的问题:“我还有移动端,不想维护两套接口。”
演讲者引用了 HTMX 官方关于拆分数据 API 与应用 API的文章,把 API 分成三类:

关键观点:
他的结论是:对他的场景,Web 返回 HTML 完全够用,数据 API 单独维护,一事一议。
演讲者反复强调:HTMX,这不是银弹。
关于性能,他也很坦诚:他的应用没有真正意义上的规模,首屏因为 HTMX 体积小会更快,但“体感上没有明显差别”;骨架屏之类的优化仍然需要自己投入精力。
演讲最后一部分,他分享了让开发顺手的工具:
| 工具 | 作用 |
|---|---|
| Task(go-task) | 一条 task dev 拉起整套本地环境 |
| Docker Compose | 启动 Postgres 等隔离依赖 |
| Air | Go 代码变更自动热重载 |
| templ / Tailwind watch | 模板与样式变更自动生成 |
| Nix 开发环境 | 所有人使用完全一致的工具版本,免去全局安装 |
| Playwright(Go 版) | 用 Go 写端到端测试,保持“全栈 Go” |
现场有观众补充:Air 本身也能执行 templ、sqlc 等构建前置任务,可能让单独的 watch 任务不再必要。演讲者表示此前并不知道这一点,感兴趣的话可以自行验证。
另外,他提到 LLM 配合 Playwright CLI 排查 Bug,“效果不错”。
回到那个烂尾的 Banter Bus:它没有被更强大的框架拯救,而是被更简单的架构拯救。
如果你是被前端折磨的后端工程师,不妨挑一个内部小工具,用 Go + HTMX 走一遍。简单,往往就是最大的生产力。
参考资料
下面是一个“植物记录”应用,只依赖 Go 标准库,数据放内存,不需要数据库。完整示例代码可以在这里下载。
环境要求:Go 1.22 及以上(用到了标准库路由的方法匹配和 r.PathValue)。浏览器需要能访问 unpkg 与 jsDelivr 两个 CDN。
项目结构:
letsgo/
├── go.mod
├── main.go
└── templates/
├── layout.html
└── partials.html
运行:
mkdir -p letsgo/templates && cd letsgo
# 把下面四个文件按路径保存后:
go run .
# 浏览器打开 http://localhost:8080
module letsgo
go 1.22.0
package main
import (
"embed"
"html/template"
"log"
"net/http"
"strconv"
"strings"
"sync"
"time"
)
//go:embed templates/*.html
var tplFS embed.FS
var tpl = template.Must(template.ParseFS(tplFS, "templates/*.html"))
// ---------- 数据层:内存存储,换成 sqlc + PostgreSQL 时只需替换这里 ----------
type Plant struct {
ID int
Name string
Health string
}
type Entry struct {
Type string
Notes string
At time.Time
}
type Store struct {
mu sync.RWMutex
plants []*Plant
entries map[int][]Entry
}
func NewStore() *Store {
return &Store{
plants: []*Plant{
{1, "薄荷", "良好"},
{2, "罗勒", "一般"},
{3, "多肉", "良好"},
},
entries: map[int][]Entry{
1: {{"浇水", "早上浇了一杯水", time.Now().Add(-48 * time.Hour)}},
},
}
}
func (s *Store) Search(q string) []*Plant {
s.mu.RLock()
defer s.mu.RUnlock()
var out []*Plant
for _, p := range s.plants {
if q == "" || strings.Contains(strings.ToLower(p.Name), strings.ToLower(q)) {
c := *p
out = append(out, &c)
}
}
return out
}
func (s *Store) Get(id int) (*Plant, bool) {
s.mu.RLock()
defer s.mu.RUnlock()
for _, p := range s.plants {
if p.ID == id {
c := *p
return &c, true
}
}
return nil, false
}
func (s *Store) SetHealth(id int, level string) (*Plant, bool) {
s.mu.Lock()
defer s.mu.Unlock()
for _, p := range s.plants {
if p.ID == id {
p.Health = level
c := *p
return &c, true
}
}
return nil, false
}
func (s *Store) Delete(id int) {
s.mu.Lock()
defer s.mu.Unlock()
for i, p := range s.plants {
if p.ID == id {
s.plants = append(s.plants[:i], s.plants[i+1:]...)
return
}
}
}
func (s *Store) AddEntry(id int, e Entry) {
s.mu.Lock()
defer s.mu.Unlock()
s.entries[id] = append([]Entry{e}, s.entries[id]...) // 新记录放最前面
}
func (s *Store) Entries(id int) []Entry {
s.mu.RLock()
defer s.mu.RUnlock()
return append([]Entry(nil), s.entries[id]...)
}
// ---------- 传输层:HTTP handler ----------
type App struct{ store *Store }
func isHX(r *http.Request) bool { return r.Header.Get("HX-Request") == "true" }
func render(w http.ResponseWriter, name string, data any) {
w.Header().Set("Content-Type", "text/html; charset=utf-8")
if err := tpl.ExecuteTemplate(w, name, data); err != nil {
log.Printf("render %s: %v", name, err)
}
}
func plantID(r *http.Request) (int, bool) {
id, err := strconv.Atoi(r.PathValue("id"))
return id, err == nil
}
// 首页:完整页面
func (a *App) index(w http.ResponseWriter, r *http.Request) {
render(w, "page", map[string]any{"Q": "", "Plants": a.store.Search("")})
}
// 搜索:同一个 URL,HTMX 请求返回片段,直接访问(刷新、分享链接)返回完整页面
func (a *App) search(w http.ResponseWriter, r *http.Request) {
q := strings.TrimSpace(r.URL.Query().Get("q"))
data := map[string]any{"Q": q, "Plants": a.store.Search(q)}
w.Header().Add("Vary", "HX-Request") // 同一 URL 两种响应,告诉缓存区分对待
if isHX(r) {
render(w, "plant-list", data)
return
}
render(w, "page", data)
}
// 详情面板(片段)
func (a *App) detail(w http.ResponseWriter, r *http.Request) {
id, _ := plantID(r)
p, ok := a.store.Get(id)
if !ok {
http.NotFound(w, r)
return
}
render(w, "detail", p)
}
// 时间线:模拟一个慢查询,配合 hx-trigger="load" 懒加载
func (a *App) timeline(w http.ResponseWriter, r *http.Request) {
id, _ := plantID(r)
time.Sleep(600 * time.Millisecond)
render(w, "timeline", map[string]any{"Entries": a.store.Entries(id)})
}
// 添加事件:成功返回时间线 + OOB 提示;失败用响应头改道到 #toast
func (a *App) addEvent(w http.ResponseWriter, r *http.Request) {
id, _ := plantID(r)
typ := strings.TrimSpace(r.FormValue("event_type"))
if typ == "" {
w.Header().Set("HX-Retarget", "#toast")
w.Header().Set("HX-Reswap", "innerHTML")
w.WriteHeader(http.StatusUnprocessableEntity)
render(w, "error-text", "事件类型不能为空")
return
}
a.store.AddEntry(id, Entry{Type: typ, Notes: strings.TrimSpace(r.FormValue("notes")), At: time.Now()})
render(w, "timeline", map[string]any{"Entries": a.store.Entries(id)})
render(w, "toast", "已记录:+"+typ)
}
// 更新健康度:一次响应同时更新列表徽标、详情徽标和提示
func (a *App) setHealth(w http.ResponseWriter, r *http.Request) {
id, _ := plantID(r)
p, ok := a.store.SetHealth(id, r.FormValue("level"))
if !ok {
http.NotFound(w, r)
return
}
render(w, "health-badge-oob", p) // 列表里的徽标
render(w, "health-badge-detail-oob", p) // 详情里的徽标
render(w, "toast", p.Name+" 的健康度已更新为 "+p.Health)
}
func (a *App) delete(w http.ResponseWriter, r *http.Request) {
id, _ := plantID(r)
a.store.Delete(id)
// 主体为空:目标 <li> 会被整个移除;同时用 OOB 更新提示
render(w, "toast", "已删除")
}
// ---------- 登录过期演示:HX-Redirect ----------
func redirect(w http.ResponseWriter, r *http.Request, url string) {
if isHX(r) {
w.Header().Set("HX-Redirect", url) // 普通 302 会被 HTMX 当成“要塞进目标里的页面”
w.WriteHeader(http.StatusOK)
return
}
http.Redirect(w, r, url, http.StatusSeeOther)
}
func (a *App) secure(w http.ResponseWriter, r *http.Request) {
if _, err := r.Cookie("session"); err != nil {
redirect(w, r, "/login")
return
}
render(w, "toast-inline", "🔓 你已登录,这是受保护的内容")
}
func (a *App) loginPage(w http.ResponseWriter, r *http.Request) { render(w, "login", nil) }
func (a *App) login(w http.ResponseWriter, r *http.Request) {
http.SetCookie(w, &http.Cookie{Name: "session", Value: "demo", Path: "/", HttpOnly: true})
http.Redirect(w, r, "/", http.StatusSeeOther)
}
func (a *App) logout(w http.ResponseWriter, r *http.Request) {
http.SetCookie(w, &http.Cookie{Name: "session", Path: "/", MaxAge: -1})
redirect(w, r, "/")
}
func main() {
a := &App{store: NewStore()}
mux := http.NewServeMux()
mux.HandleFunc("GET /{$}", a.index)
mux.HandleFunc("GET /plants", a.search)
mux.HandleFunc("GET /plants/{id}", a.detail)
mux.HandleFunc("GET /plants/{id}/timeline", a.timeline)
mux.HandleFunc("POST /plants/{id}/events", a.addEvent)
mux.HandleFunc("POST /plants/{id}/health", a.setHealth)
mux.HandleFunc("DELETE /plants/{id}", a.delete)
mux.HandleFunc("GET /secure", a.secure)
mux.HandleFunc("GET /login", a.loginPage)
mux.HandleFunc("POST /login", a.login)
mux.HandleFunc("POST /logout", a.logout)
log.Println("listening on http://localhost:8080")
log.Fatal(http.ListenAndServe(":8080", mux))
}
{{define "page"}}<!doctype html>
<html lang="zh-CN">
<head>
<meta charset="utf-8">
<meta name="viewport" content="width=device-width, initial-scale=1">
<title>Let's Go 植物记录</title>
<!-- 让 422 响应也参与替换,这样表单校验错误可以直接显示 -->
<meta name="htmx-config" content='{"responseHandling":[{"code":"204","swap":false},{"code":"[23]..","swap":true},{"code":"422","swap":true},{"code":"[45]..","swap":false,"error":true}]}'>
<script src="https://unpkg.com/[email protected]"></script>
<script defer src="https://cdn.jsdelivr.net/npm/[email protected]/dist/cdn.min.js"></script>
<style>
body{font-family:system-ui,sans-serif;max-width:640px;margin:2rem auto;padding:0 1rem;line-height:1.6}
[x-cloak]{display:none!important}
ul{padding-left:1.2rem} li{margin:.4rem 0}
.badge{padding:.1rem .5rem;border-radius:999px;font-size:.85rem;background:#e5e7eb}
.良好{background:#bbf7d0}.一般{background:#fde68a}.枯萎{background:#fecaca}
#toast{min-height:1.5rem;color:#065f46;margin:.5rem 0}
.err{color:#b91c1c}
input,textarea,button{font:inherit;margin:.15rem 0}
.htmx-request{opacity:.5}
</style>
</head>
<body>
<h1>🌱 Let's Go 植物记录</h1>
<div id="toast"></div>
<input type="search" name="q" value="{{.Q}}" placeholder="搜索植物,比如:薄荷"
hx-get="/plants"
hx-trigger="input changed delay:300ms, search"
hx-target="#plant-list"
hx-push-url="true">
<div id="plant-list">{{template "plant-list" .}}</div>
<div id="detail"></div>
<hr>
<button hx-get="/secure" hx-target="#secure-result">模拟:请求受保护内容</button>
<span id="secure-result"></span>
</body>
</html>{{end}}
{{define "plant-list"}}<ul>
{{range .Plants}}{{template "plant-item" .}}
{{else}}<li>没有找到匹配的植物</li>
{{end}}</ul>{{end}}
{{define "plant-item"}}<li id="plant-{{.ID}}">
<strong>{{.Name}}</strong> {{template "health-badge" .}}
<button hx-get="/plants/{{.ID}}" hx-target="#detail">查看</button>
<span x-data="{ open: false }">
<button x-show="!open" @click="open = true">删除</button>
<span x-show="open" x-cloak>
确定删除?
<button hx-delete="/plants/{{.ID}}" hx-target="#plant-{{.ID}}" hx-swap="outerHTML">确认</button>
<button @click="open = false">取消</button>
</span>
</span>
</li>{{end}}
{{define "health-badge"}}<span id="health-{{.ID}}" class="badge {{.Health}}">{{.Health}}</span>{{end}}
{{define "health-badge-oob"}}<span id="health-{{.ID}}" class="badge {{.Health}}" hx-swap-oob="true">{{.Health}}</span>{{end}}
{{define "health-badge-detail-oob"}}<span id="detail-health-{{.ID}}" class="badge {{.Health}}" hx-swap-oob="true">{{.Health}}</span>{{end}}
{{define "toast"}}<div id="toast" hx-swap-oob="true">{{.}}</div>{{end}}
{{define "error-text"}}<span class="err">{{.}}</span>{{end}}
{{define "toast-inline"}}{{.}}{{end}}
{{define "detail"}}<section>
<h2>{{.Name}} <span id="detail-health-{{.ID}}" class="badge {{.Health}}">{{.Health}}</span></h2>
<div>
<button hx-post="/plants/{{.ID}}/health" hx-vals='{"level":"良好"}' hx-swap="none">标记:良好</button>
<button hx-post="/plants/{{.ID}}/health" hx-vals='{"level":"一般"}' hx-swap="none">标记:一般</button>
<button hx-post="/plants/{{.ID}}/health" hx-vals='{"level":"枯萎"}' hx-swap="none">标记:枯萎</button>
</div>
<form hx-post="/plants/{{.ID}}/events" hx-target="#timeline"
hx-on::after-request="if (event.detail.successful) this.reset()">
<input name="event_type" placeholder="事件类型:浇水 / 换盆 / 施肥">
<br>
<textarea name="notes" placeholder="备注(可选)" rows="2" cols="40"></textarea>
<br>
<button type="submit">记录</button>
</form>
<h3>时间线</h3>
<div id="timeline" hx-get="/plants/{{.ID}}/timeline" hx-trigger="load">加载中……</div>
</section>{{end}}
{{define "timeline"}}<ul>
{{range .Entries}}<li>{{.At.Format "01-02 15:04"}} · <strong>{{.Type}}</strong>{{if .Notes}}:{{.Notes}}{{end}}</li>
{{else}}<li>还没有记录</li>
{{end}}</ul>{{end}}
{{define "login"}}<!doctype html>
<html lang="zh-CN"><head><meta charset="utf-8"><title>登录</title></head>
<body style="font-family:system-ui;max-width:420px;margin:3rem auto">
<h1>请先登录</h1>
<p>(演示:点击按钮即写入 session Cookie)</p>
<form method="post" action="/login"><button type="submit">登录</button></form>
</body></html>{{end}}
建议按下面的顺序操作,每一步对应文章里的一个知识点:
/plants?q=薄,复制这个链接在新标签页打开,会得到完整页面,这就是同一个地址对 HTMX 请求和普通访问返回不同内容。hx-trigger="load" 加服务端模拟慢查询的效果。HX-Retarget 改了更新位置。打开浏览器开发者工具的 Network 面板,可以看到所有 HTMX 请求的响应体都是 HTML 片段而不是 JSON。点开请求,还能在请求头里看到 HX-Request: true,在响应头里看到 HX-Retarget、HX-Redirect 等控制头。
还在为“复制粘贴喂AI”而烦恼?我的新专栏 《AI原生开发工作流实战》 将带你:
扫描下方二维码,开启你的AI原生开发之旅。

你的Go技能,是否也卡在了“熟练”到“精通”的瓶颈期?
继《Go语言第一课》后,我的《Go语言进阶课》终于在极客时间与大家见面了!
我的全新极客时间专栏 《Tony Bai·Go语言进阶课》就是为这样的你量身打造!30+讲硬核内容,带你夯实语法认知,提升设计思维,锻造工程实践能力,更有实战项目串讲。
目标只有一个:助你完成从“Go熟练工”到“Go专家”的蜕变! 现在就加入,让你的Go技能再上一个新台阶!

商务合作方式:撰稿、出书、培训、在线课程、合伙创业、咨询、广告合作。如有需求,请扫描下方公众号二维码,与我私信联系。

2026-10-20 06:00:00
本文永久链接 – https://tonybai.com/2026/10/20/go-net-http-server-handlerequest-accepted
大家好,我是Tony Bai。
【导读】
Go 提案评审组刚刚把 #77441 标记为 accepted。
它只给 net/http.Server 加一个方法,签名也只有一行,却直指一个正在逼近的问题:HTTP/3 来了,第三方协议实现该如何复用标准库 Server 里那段“看不见的中间件”?
这个提案名字改了一次,签名也改了一次。本文带你看懂它的来龙去脉和设计取舍。
【文章要点】
Server.HandleRequest(ResponseWriter, *Request) error。OPTIONS *、DefaultServeMux 兜底和 panic 恢复。ServeHTTP 到 HandleRequest,从无返回值到返回 error。CrossOriginProtection 等 Server 级默认行为,都可以挂在这条路径上。
最近的 Go 提案评审会议纪要里,有一条很不起眼的记录:
net/http: add Server.HandleRequest #77441,accepted 🎉
乍一看,它只是给 http.Server 加了一个方法:
func (*Server) HandleRequest(ResponseWriter, *Request) error
没有新语法,没有泛型,也没有性能数字。
但如果你关心 Go 的网络栈演进,尤其是 HTTP/3 在 Go 里怎么落地,这个提案值得认真读一遍。它解决的是一个很现实的工程问题:
当请求不是由 net/http.Server 自己从连接上读出来的,怎么让它享受 Server 内部那层处理逻辑?
下面一步步拆解。
http.Server 里怎么走我们写 Go HTTP 服务,通常只关心自己的 Handler。但请求在到达 Handler 之前,其实经过了好几步。
据提案作者 Damien Neil(neild)的描述,请求流转大致如下:
OPTIONS * 请求(可通过 Server.DisableGeneralOptionsHandler 关闭);Server.Handler,如果它为 nil 则使用 http.DefaultServeMux;http.ServeMux),最后才是叶子 Handler。用图来表示:

图中黄色的“Server 内部处理层”,就是这个提案的主角。
它平时很低调,因为你无法直接调用它。要触发它,只有一个办法:让请求真的从连接上读进来。
提案的“动机案例”写得很直白:
设想一个 HTTP/3 服务器,有一个 ServePacketConn 方法,用来在 net.PacketConn(UDP)上开始服务。它同样会读出请求、构造 *http.Request,然后呢?
它得自己再实现一遍:
OPTIONS * 怎么回;Handler 为 nil 时怎么兜底;提案评审时的讨论也印证了这个历史包袱。据 Austin Clements(aclements)总结:
也就是说,Go 团队自己就为这个问题付过“复制代码”的代价。HTTP/3 如果再来一次,既是重复劳动,也会带来行为不一致的风险。

提案文本的核心思想是:把这层内部逻辑公开出来,让任何拿到 *http.Request 的代码,都能当作“该 Server 收到了这个请求”来处理。
根据最新修订后的文档,行为如下:
Server.DisableGeneralOptionsHandler 不为 true,对 OPTIONS * 请求返回 200 OK 且 Content-Length: 0;Server.Handler 为 nil,使用 http.DefaultServeMux;ErrAbortHandler,则记录日志;ErrAbortHandler,则返回 ErrAbortHandler。签名为:
func (*Server) HandleRequest(ResponseWriter, *Request) error
说明:提案讨论中的细节在不同阶段有调整,以上以评审讨论中的最新修订为准。具体文档措辞以最终合入 Go 源码的版本为准。
这个提案的演进过程,本身就是一堂 API 设计课。
ServeHTTP → HandleRequest
最初的提案叫 Server.ServeHTTP。听上去顺理成章,因为 Go 里的 http.Handler 就是 ServeHTTP。
但问题也在这里。社区成员指出:
ServeHTTP,容易让人误以为 *http.Server 现在是一个 http.Handler,可以直接拿去当 Handler 挂到别处;http.Serve、http.ServeTLS。而它的实际定位是:
我已经拿到了一个请求,请按“这个 Server 收到了它”来处理。
作者最终采纳了 HandleRequest 这个名字。它更直白,也不会让人把它误当作生产路径上的 Handler。
error
作者的修订理由很务实:能知道 Handler 是否 panic 过,是有用的信息。
比如在测试里,你想断言“这个请求会触发 panic”,只靠恢复后静默吞掉是不够的。
同时,作者特意说明了边界:
ErrAbortHandler 例外,因为它在 Handler 语义里有明确含义;type HandlerPanicError struct { PanicValue any }
这是典型的 Go 风格:先把最小可用的东西做对,把扩展空间留在未来。
顺便一提,多出来的 error 返回值,也让它自然地不满足 http.Handler 接口。这在无意中呼应了作者的意图:它不是用来挂到 Server 上当 Handler 的。
提案讨论里有三个有代表性的观点,都值得一看。
有成员担心,HandleRequest 这个名字会让人误以为可以在生产代码里随便用,而它本意是让协议实现者和测试代码复用 Server 的行为。
有人提出另一种形态:
func (s *Server) Preprocess(h http.Handler) http.Handler
即“传入一个 Handler,返回包装后的 Handler”。
作者回应得很干脆:这是完全不同的事情。
另一位讨论者也提出,两种形态在使用上本质等价:
server.ServerHandler()(resp, req)
server.HandleRequest(resp, req)
区别只在于调用方更倾向于保存一个 Handler,还是保存整个 Server。
评审会上的判断很坦率:
也就是说,这不是一个面向业务开发者的“大众 API”,而是写给基础设施作者的“工具接口”。
下面代码为示意,帮助理解使用方式,不代表官方示例。
过去我们常用 httptest.NewRecorder 直接调用 Handler:
rec := httptest.NewRecorder()
handler.ServeHTTP(rec, req)
这样测不到 Server 层的行为,比如 OPTIONS * 的处理,以及 Handler panic 时的恢复。
有了 HandleRequest,可以这样写:
srv := &http.Server{Handler: mux}
req := httptest.NewRequest("OPTIONS", "*", nil)
rec := httptest.NewRecorder()
if err := srv.HandleRequest(rec, req); err != nil {
t.Fatalf("unexpected error: %v", err)
}
// 验证:未关闭 General Options Handler 时,应返回 200 且 Content-Length 为 0
测 panic 行为同样直观:
srv := &http.Server{
Handler: http.HandlerFunc(func(w http.ResponseWriter, r *http.Request) {
panic("boom")
}),
}
err := srv.HandleRequest(httptest.NewRecorder(), httptest.NewRequest("GET", "/", nil))
if err == nil {
t.Fatal("expected error from panicking handler")
}
设想一个 HTTP/3 实现,读出请求后不再自己写中间件逻辑,而是直接委托:
func (h3 *h3Server) serveStream(w http.ResponseWriter, r *http.Request) {
// 读取并构造好 *http.Request 之后:
_ = h3.base.HandleRequest(w, r) // base 为 *http.Server
}
这样,OPTIONS * 的处理、Handler == nil 的兜底、panic 恢复与日志,都与 HTTP/1、HTTP/2 保持一致。

这个提案真正有想象空间的地方,在于作者的一句话:
现在这层内部 Handler 做的事情不多,但预计未来会更多。
提案里提到了一个例子:此前讨论过,要不要给 Server 增加一个开关,对整个 Server 默认启用 http.CrossOriginProtection,也就是跨站请求保护。相关讨论见 #73626。
一旦 Server 级的默认行为变多,如果没有这个统一入口,每一种协议实现都要手动追加这些行为,既容易漏,也容易不一致。
评审会上还有一个很有说服力的观察:
http.Server 的大部分字段,都是在配置“如何把连接上的字节变成 Request”;这说明“连接上的字节 → Request”与“Request → Handler”这两步的边界划分是相当完整的。只把后一步暴露出来,抽象上是自洽的。
此外,从评审纪要看,与之相关的 net/http: pluggable HTTP/3(#77440)和 x/net/http3: add experimental HTTP/3 implementation(#70914)目前处于 hold 状态。这也提醒我们:HandleRequest 是一块先落地的基础拼图,HTTP/3 的整体方案仍在推进中。
先说结论:大多数人短期内不会直接用到它。
但它仍然有价值:
需要注意的几点:
Server.Handler 里当 Handler 用;这个提案的魅力,在于它的克制:
一句话总结:Go 把 http.Server 里“请求到 Handler 之间”那段看不见的路,修成了一条可以名正言顺调用的官方通道。
参考资料
还在为写 Agent 框架频频死循环、上下文爆炸而束手无策?我的新专栏 《从0 开始构建 Agent Harness》 将带你:
扫描下方二维码,开启从 0 开始构建Agent Harness 的实战之旅。

你的Go技能,是否也卡在了“熟练”到“精通”的瓶颈期?
继《Go语言第一课》后,我的《Go语言进阶课》终于在极客时间与大家见面了!
我的全新极客时间专栏 《Tony Bai·Go语言进阶课》就是为这样的你量身打造!30+讲硬核内容,带你夯实语法认知,提升设计思维,锻造工程实践能力,更有实战项目串讲。
目标只有一个:助你完成从“Go熟练工”到“Go专家”的蜕变! 现在就加入,让你的Go技能再上一个新台阶!

商务合作方式:撰稿、出书、培训、在线课程、合伙创业、咨询、广告合作。如有需求,请扫描下方公众号二维码,与我私信联系。

2026-10-19 12:00:00
本文永久链接 – https://tonybai.com/2026/10/19/harness2-recursive-agent-harnessing-google-research
大家好,我是Tony Bai。
【导读】
同一个模型,换一套“Harness”,成绩就能差出十几分。谷歌研究团队最近发布 Harness²,让 Agent 在没有标准答案的情况下,自己诊断、自己改装、自己总结经验,而且改装经验还能留给下一个任务用。一步改进,GLM-5 在 WorkBuddy-Bench 上平均提升 11.5 分,反超了原版 Gemini 3.5 Flash。代码已开源。
【文章要点】

今天做 Agent 的人,几乎都有过这样的体验:同一个模型,放进不同的工具框架里,表现可以差得很远。
这个“框架”,业界现在叫 Harness(外壳):提示词、记忆、技能、工具说明、子 Agent 编排,都算在内。近期流行的一个说法是:Agent = 模型 + Harness。
问题来了:Harness谁来调?
人工调,费时费力。让 AI 自己调,也就是递归自我改进(RSI),听上去很美,但落到真实场景就卡壳。
论文把现有方法的困境归结为两点。
第一,没有标准答案。
开放世界里的任务,设计Harness时见都没见过,运行时又全是新的,既没有真值,也没有可靠的验证器。你怎么知道刚才那处修改是真的变好,还是碰巧?
第二,经验无法沉淀。
为任务 A 精心改出来的Harness,换到任务 B 往往水土不服。直接继承上一个Harness,还会在任务分布变化时引入噪声。
但论文指出了一个被忽视的事实:改进的过程本身就是宝贵的经验,比如问题怎么诊断、试了哪些改动、执行后发现了什么。这些东西,应该被留下来。
于是他们提出了核心问题:
递归自我改进,能不能既改进当前的Harness,也改进“以后怎么改Harness”?
名字里的上标 2,指的就是“两层”。整体流程如下:

这是整个框架的发动机,一步分三环:
关键点在于:论文明确说,这些对照是为合成提供依据,并不验证答案对不对。因为执行有随机性,模型也有共同偏见,它是证据,不是裁判。

用一个预算参数 k 控制探索量:

并行递归一次性铺开,再让多个合成会话各自融合;串行递归把上一步的Harness和执行证据一路传给下一步,后面的步骤可以修正前面的改动。k=1 时两者等价。

每个任务结束后,系统会复盘整个改进记录,把被采纳的Harness和有证据支持的经验存进改进库。库里每个条目包含一个可执行Harness,加一份记录适用场景、经验教训和证据的 EXPERIENCE.md。
注意两个细节:
被改动的Harness有 8 类可编辑组件:系统提示词、护栏、记忆、技能、工具说明、脚本、子 Agent、中间件插件。每个组件都以文件形式挂载在运行时里,改动就是改文件。

实验在三个专业基准上进行:WorkBuddy-Bench(代码、网页、办公)、JobBench(端到端工作任务)、LAB(法律工作,指标为逐条标准通过率 Partial)。执行模型是 Gemini 3.5 Flash 和 GLM-5,每个模型都跑在 OpenCode 和 Codex 两种Harness下,共 4 种配置。默认的Harness编辑器是 Claude Opus 4.8。
下表摘自论文,为单步改进(k=1)相对基础Harness的变化:
| 配置 | WorkBuddy 平均分 | JobBench 分数 | LAB Partial |
|---|---|---|---|
| GLM-5 + OpenCode | 64.2 → 75.7(+11.5) | 20.6 → 24.2(+3.6) | 59.6 → 71.4(+11.8) |
| GLM-5 + Codex | 64.4 → 75.3(+10.9) | 23.6 → 24.8(+1.2) | 58.1 → 65.9(+7.8) |
| Gemini 3.5 Flash + OpenCode | 72.4 → 77.5(+5.1) | 31.5 → 36.0(+4.5) | 79.9 → 81.9(+2.0) |
| Gemini 3.5 Flash + Codex | 74.5 → 77.5(+3.0) | 33.9 → 35.3(+1.4) | 71.6 → 75.6(+4.0) |
几个值得拎出来的结论:
① 四种配置全部提升。 最大涨幅分别是 WorkBuddy +11.5、JobBench +4.5、LAB +11.8个百分点。
② 弱模型受益更大,甚至能反超。 在 WorkBuddy 上,GLM-5 经过一步改进后拿到 75.7(OpenCode)和 75.3(Codex),超过了 Gemini 3.5 Flash 的原始成绩 72.4 和 74.5。弱模型配上改进后的Harness,可以超过强模型用原Harness。
③ 对手不太稳。 论文称,ReasoningBank 在代码任务上最多比基础Harness低 6.6 分;Harness Scaling 在 12 组“基准—配置”里有 7 组低于基础Harness。Harness²在 WorkBuddy 平均分和 JobBench 分数上,4 种配置全部超过所比较的基线。
④ 加预算继续涨。 并行递归 k=5,在单步基础上再涨:WorkBuddy +2.9 至 3.9,JobBench +3.0 至 4.2,LAB +2.6 至 6.7个百分点。以 Gemini 3.5 Flash + OpenCode 为例,k 从 1 增加到 5,相对基础Harness的收益在 JobBench 上从 4.5 升到 7.5,在 WorkBuddy 上从 5.1 升到 8.4。
⑤ 步数更少。 在 WorkBuddy 上,Harness²的平均执行步数大多低于或接近基线,说明提升不是靠“多跑几步”换来的。论文还提到,在算力与性能的权衡图上,Harness²的两种配置都落在经验帕累托前沿上。
消融实验(Gemini 3.5 Flash + OpenCode,k=1):
| 版本 | WorkBuddy | JobBench |
|---|---|---|
| 完整 Harness² | 77.5 | 36.0 |
| 去掉改进库 | 74.4 | 34.2 |
| 去掉范围划分(通用/领域两类编辑器合并为泛化编辑器) | 74.6 | 32.3 |
| 去掉合成(只选一个候选) | 75.9 | 34.1 |
三个设计都有贡献。其中“范围划分”在 JobBench 上影响最大,掉了 3.7 分。
“直接改”不行,有库才行。
论文做了个对比:不给参考执行、不给候选探测、也不给改进库,直接让编辑器改基础Harness,结果反而退步:Code 从 73.4 掉到 63.2,Web 从 69.9 掉到 65.0。k=1 积累出的改进库能把性能拉回基础水平,k=5 积累的库则带来 Code +0.9、Web +4.4、Office +5.1 的增益。探索越充分,沉淀出的经验越值钱。
经验可以跨基准迁移。
用 JobBench 积累的库去帮 WorkBuddy 做单步改进,三个领域分别有 +0.6、+0.5、+2.9 的提升。不过论文也说明,这是回顾性测试,用于验证跨任务复用,而不是在线适应。
编辑器不必更强。
主实验用 Opus 4.8 做编辑器,难免让人怀疑“是不是强模型教弱模型”。论文给了同模型自我改进的实验:从 GLM-5 到 Claude Opus 5,五个模型在每个基准上都有提升;Opus 5 在三个基准上分别 +3.3、+5.5、+3.0,GLM-5 在 LAB 上 +13.7。
论文给了一个 JobBench 的案例(Gemini 3.5 Flash + OpenCode)。基础Harness得分 43.1,轨迹显示失败原因不是知识缺失,而是流程缺陷:多个源文件的数据没有对账,产出文件写完后也没有重新打开检查。
Harness²做了两处针对性改动:
合成阶段对照参考执行后,四处改动全部保留。重跑之后,数据完成交叉核对,备忘录缺失的章节被补齐,得分升到 77.8。

仓库为 Apache-2.0 协议,要求 Linux、Python 3.12 和 uv。无需模型凭证就能跑本地演示:
uv venv --python 3.12 .venv
source .venv/bin/activate
uv pip install -e '.[render]'
harness2-demo --output runs/demo --k 2
演示用确定性编辑器和真实 Python 执行,同时展示两种递归模式。要跑真实基准,需要 Node.js 20+、Google Cloud CLI,并配置 Vertex AI 项目。以 LAB 为例:
harness2-setup lab
harness2 --bench lab --k 1 --mode parallel --only-domains antitrust-competition --max-tasks 1
harness2-judge --bench lab --k 1 --mode parallel
harness2-report --bench lab --k 1 --mode parallel
--k 是任务级递归预算,--mode 选并行或串行,--substrate cx 切换到 Codex 执行器,--dry-run 可以先预览任务选择而不调用模型。运行结果会保存在 runs/ 下,包括交付物、被采纳的Harness、反思笔记和评测结果,重复同一命令即可断点续跑。
Harness²给出的思路很清晰:模型权重不动,把“怎么改Harness”本身也当成可学习的对象。它不依赖标准答案,靠同一任务下的行为对照做判断;它不盲目继承旧Harness,而是把经验和证据存起来,按需调用。
当模型能力逐渐拉不开差距,Harness工程可能成为下一个拉开差距的地方。至于这套“自己改装自己”的机制,能在多大范围内稳定复现,还有待社区用真实业务来检验。
资料来源
还在为写 Agent 框架频频死循环、上下文爆炸而束手无策?我的新专栏 《从0 开始构建 Agent Harness》 将带你:
扫描下方二维码,开启从 0 开始构建Agent Harness 的实战之旅。

还在为“复制粘贴喂AI”而烦恼?我的新专栏 《AI原生开发工作流实战》 将带你:
扫描下方二维码,开启你的AI原生开发之旅。

商务合作方式:撰稿、出书、培训、在线课程、合伙创业、咨询、广告合作。如有需求,请扫描下方公众号二维码,与我私信联系。

2026-10-19 06:00:00
本文永久链接 – https://tonybai.com/2026/10/19/gophercon-eu-2026-go-team-panel
大家好,我是Tony Bai。
【导读】
AI 找漏洞的本事越来越强,最先“遭殃”的,其实是维护者。GopherCon EU 2026 的 Go 团队圆桌上,安全团队负责人 Roland Shoemaker 说,团队每月收到的安全报告,已经从最糟糕时的 5~10 份,涨到了 100~200 份。他还有一句大实话:“我的团队压力大得多,大家都睡得少了。”
这场圆桌只有半小时,信息量却很大。两位嘉宾一位是 Go 安全团队负责人,一位是 log/slog 的作者之一、现在主攻 Go 的 iter、集合类库与包站点 API 的 Jonathan Amsterdam。这篇文章,我们把对话拆开,结合 Go 1.26/1.27 的发布说明和行业数据,看看 Go 团队在 AI 时代到底怎么想、怎么做。
【文章要点】
crypto/mldsa)、SIMD、高层密码学 API、对 LLM 友好的生态。
先认识一下 Roland 的团队。
他自己的说法是:“我们把工作做好的标志,就是没人知道我们存在。”
具体干什么?
crypto/x509、crypto/tls、net、net/http、encoding/json……基本就是“一个生产服务需要的全套栈”。他们的设计信条也很朴素:尽量不要给用户“带刃的 API”,让做错事变得很难。
这也解释了为什么,当 AI 开始大规模“挖洞”,这个团队是最先感受到压力的人之一。
Roland 给出了一组很直观的数字:
| 时间 | 每月安全报告量 |
|---|---|
| 过去(糟糕的月份) | 约 5~10 份 |
| 现在 | 约 100~200 份 |
同时他强调,这里面很多其实是 Bug 报告,而不是安全报告。原因有两类:
这不是 Go 一家的遭遇,行业数据也在印证:
需要说明:行业数据的成因并不全是 AI,GTIG 的报告自己也强调不能把所有增长都归因于 AI。
Roland 透露了三个方向,我整理成一张图:

① 重新分级。
过去报告少,每一份都能按最高优先级处理。现在不行了。比如,给一个解析 API 喂入畸形输入导致 panic,虽然“让 Go 程序崩溃不是好事”,但它和“绕过工具链里的数据库校验”完全不是一个量级。Roland 的判断是:这种局面下,更多问题会在修复之前就变成公开的。
② 内部提效。
用 LLM 主动做检测,同时用它帮忙处理报告本身,从“被动响应”变成“主动发现”。
③ 左移。
这是我最喜欢的一点:安全报告之所以存在,是因为有 Bug 进了标准库。所以更好的办法,是在 Bug 进来之前就拦住。他提到的方向,是让 CI 里的机器人跑 LLM 工具,但“具体长什么样,我们还没完全想清楚”。
Linux 内核的立场,据 Roland 转述,是所有 AI 发现的安全 Bug 都应该公开,理由是“你能跑这个工具,别人也能跑”。
Roland 的回答很干脆:“这会让我的生活轻松很多,但会让很多别人的生活难很多。”
Jonathan 在旁边补了一刀:“这也不完全成立,因为 Mythos 目前只开放给少数人。”
这句调侃背后是个真问题:如果最强的漏洞挖掘模型并不是人人可用,那么“反正大家都能发现”就不成立,负责任披露依然有它的价值。
主持人问的第一个问题,很接地气:你们自己用 AI 吗?
两位都用,而且都用 Google 的内部工具(Antigravity 和 Gemini)。但风格迥异。
Roland:少用。
他做的是必须“完全吃透”的代码,AI 一口气吐出几百行,他没时间逐行看,“往往自己写更快”。不过,他们正在更多地把 AI 用于漏洞分析,认为还有很多工作要做,但已经“相当有用”。
Jonathan:当初级工程师用。
他主要用在三类场景:
他分享的那个 skill,我觉得值得抄作业:

关键点只有一个:每一轮都停下来,让人确认。
Jonathan 的原则是:一切都是建议性的(advisory)。他不会说“AI 写了一个 1 万行的程序,我一行都没看”——“我还没到那一步”。
主持人问:你觉得 Go 最缺什么?答案是一串关键词。
Roland 说,安全方向最担心的是“即将到来的后量子末日”,团队在 1.27 和 1.28 中重点准备签名相关的包。
时间线对得上:Go 1.27 已于 2026 年 8 月 19 日发布,新增 crypto/mldsa 包,实现 FIPS 204 标准的 ML-DSA 后量子签名,并集成进了 crypto/x509 和 crypto/tls。这件事的前置工作,其实在 Go 1.26 就以内部实现的形式做好了。
Jonathan 说 SIMD 会“打开一整类应用场景”,而且现在就能用实验标志体验。
确实如此。Go 1.26 引入了实验性的 simd/archsimd 包,需要在构建时设置环境变量:
GOEXPERIMENT=simd go build ./...
Go 1.27 的发布博客里,simd 与 simd/archsimd 仍标注为“实验性”支持。
这是 Roland 个人最想改善的点。Go 早期的密码学 API,是为“真正懂密码学的人”设计的,对大多数人来说是带刃的,需要大量研究才能用对。
方向是提供更高层的 API,类似:
“给你一个 Reader,我们还你密文,用的就是我们认为最安全的方式。你不需要做任何选择。”
这是 Jonathan 的一个判断:让语言、生态、标准库和工具对 LLM 更友好,虽然这件事“变化得非常快”。
他正在做的包站点(pkg.go.dev)API,目前已有 Beta 版,设计时就考虑了 LLM:比如提供可直接下载的 OpenAPI 文档,文档本身既是人类可读的,也是 LLM 可读的。
他还特别指出,这类设计往往“对人友好的,也就对 LLM 友好”,两者重合度很高。
有观众问 MCP SDK 什么时候发布,答案是“已经发布了”:github.com/modelcontextprotocol/go-sdk。Jonathan 是原作者之一,现在由 Google 的另一支更偏生产运维的团队维护,他本人只做顾问。
这里有个有趣的细节:他说,Go 团队并不是“生产团队”,除了模块代理和包站点,基本不运维生产系统。所以他们把 SDK 孵化出来,再交给更合适的人。从 GitHub 仓库看,SDK 已发布稳定的 v1.x 版本,并持续跟进 MCP 规范版本。
Go 团队有多小?主持人说“曾经可能只有 30 人”,Jonathan 说,“具体不公开,但是是两位数”。
一年两次发布、人数两位数,必然要极度克制。他们的几条原则:
1. 每一个新 API,都是永远的承诺。
Roland 说:每加一个包,就意味着要永远维护。所以提案审查时,核心问题不是“有它好不好”,而是“我们有没有时间长期维护,它是否持续产生价值”。
Jonathan 引用了 Rob Pike 教他的话:
“No is temporary, yes is forever.”(“不”是暂时的,“好”是永远的。)
2. 不是所有东西都该进标准库。
Roland 的原话大意是:标准库大是 Go 最好的特点之一,但这也是巨大的责任,因为不能破坏兼容性。
3. 把更多工作交给社区。
Jonathan 说,团队正在扩大社区在“开发 Go 本身”上的角色:更高效地审 CL(也就是 PR)、清理 issue 积压,并把部分工作委托出去,比如包含外部贡献者的“集合工作组”。
两位嘉宾的建议很实在:
help wanted 标签或者你熟悉的 issue 开始;还有一个坦率的提醒:Go 目前没法“认领” issue,任何人都可能抢先提交 CL,即使提了 CL,团队也不保证很快审。这是流程的缺陷,但现实如此。
圆桌后半段是语言设计问答,三个问题,Jonathan 都讲得很透。
答案不是“感觉不对”,而是一个架构原则:
语言不应该依赖标准库。
如果内置 map 依赖标准库里定义的某个接口,就等于语言依赖了标准库。
有人反问:error 接口不就在标准库里吗?Jonathan 的回答是,error 在语言里其实只是一个普通接口,语言并不关心你是否返回它,你甚至可以把 error 当第一个返回值。至于格式化错误的特殊处理,那是 fmt 包的事。
他还幽默地补了一句:“就算有反例,也不意味着我们要再加一个。”
Jonathan 的回答是:“我们已经有了,叫指针。”
当然也可以用泛型写一个 Optional[T],但实践中,encoding/json、Google Cloud API 等都用指针表示可选。
为了让指针更好用,Go 1.26 做了一个小改进:new 现在可以接受表达式。
// Go 1.26 之前
age := yearsSince(born)
p := Person{Name: "Gopher", Age: &age}
// Go 1.26 起
p := Person{Name: "Gopher", Age: new(yearsSince(born))}
这是被企业开发者问得最多的问题。Jonathan 的回应相当长,核心是四个“复杂度炸弹”:

Roland 补充说,Go 团队内部每次聚会,这几个话题都会重复出现,“每次都觉得要是能有就好了,但一想真实的样子,就变成一团糟”。
Jonathan 的立场很明确:
Go 因为泛型、迭代器变复杂了一些,但它仍然是最简单的主流编程语言,我们要让它继续如此。我们不想变成 Rust 或 C++。(不是它们不好,只是“不是我们想住的地方”。)
主持人感叹 Rob Pike 能以学术高度为“普通开发者”设计语言。Jonathan 立刻纠正了一个误解:
“普通”不是“笨”。“普通”指的是每一个人,包括一年后回头看自己代码的你。
他还讲了一个小故事:自己曾写过一个“自以为很聪明”的改动,评审者提醒他:“想想两三年后你来维护它的时候。”他承认,确实存在一种不那么聪明、但更正确的写法。
他引用了 Brian Kernighan 的名言,大意是:写出那段极其聪明代码的你,永远比调试它的你更聪明,哪怕是同一个人。
最后一个问题很轻松:Go Gopher 吉祥物是谁创作的?
答案是 Renee French。她同时是 Rob Pike 的伴侣,也是一位严肃的艺术家,还为其他语言做过吉祥物,但 Gopher 无疑是她的代表作。Jonathan 还推荐了她在 GopherCon 2016 上的非技术分享,据说“非常有趣”。
回看这场圆桌,我认为有三点,比任何一个具体特性都更值得记住。
1. AI 正在改变“信号与噪声”的比例,而不只是改变效率。
漏洞挖掘变得廉价,但读报告的人没有变得廉价。Go 团队的应对是:重新分级、提效、左移,不放弃负责任披露。这个思路,对任何开源维护者都有参考价值。
2. “克制”本身就是一种能力。
每一个 API 都是永远的承诺,每一个语言特性都有复杂度的税。Go 能保持“最简单的主流语言”,靠的不是不会做,而是知道不做什么。
3. 人要始终在回路里。
不管是写测试还是做漏洞分析,两位嘉宾的共识是:AI 是初级工程师,不是架构师。让它多干活,但每一步留一个“停下来给我看”的检查点。
最后留一个问题给你:如果你维护的项目,今天突然每月多收到 100 份“看起来很专业”的报告,你会怎么办?
参考资料
还在为“复制粘贴喂AI”而烦恼?我的新专栏 《AI原生开发工作流实战》 将带你:
扫描下方二维码,开启你的AI原生开发之旅。

你的Go技能,是否也卡在了“熟练”到“精通”的瓶颈期?
继《Go语言第一课》后,我的《Go语言进阶课》终于在极客时间与大家见面了!
我的全新极客时间专栏 《Tony Bai·Go语言进阶课》就是为这样的你量身打造!30+讲硬核内容,带你夯实语法认知,提升设计思维,锻造工程实践能力,更有实战项目串讲。
目标只有一个:助你完成从“Go熟练工”到“Go专家”的蜕变! 现在就加入,让你的Go技能再上一个新台阶!

商务合作方式:撰稿、出书、培训、在线课程、合伙创业、咨询、广告合作。如有需求,请扫描下方公众号二维码,与我私信联系。

2026-10-18 07:30:00
本文永久链接 – https://tonybai.com/2026/10/18/verus-rust-formal-verification-amazon-nitro
大家好,我是Tony Bai。
【导读】
Rust的类型系统能防内存越界、防数据竞争,但它证明不了“代码算出来的结果是对的”。亚马逊选择用一套叫Verus的开源工具,把Rust代码直接变成可以被数学证明的对象——不用切换语言,不用另起炉灶,甚至连unsafe代码和并发锁都能证明“绝对正确”。这套武器已经被用在AWS Nitro隔离引擎的核心组件上。
【文章要点】

这些年,Rust凭借接近C语言的性能,加上编译期就能拦截内存错误的类型系统,已经拿下了不少工业界的关键基础设施。在亚马逊内部,Firecracker(支撑AWS Lambda和Fargate的微虚拟机方案)、内部的无服务器分布式SQL数据库,以及为Nitro Hypervisor提供虚拟机隔离能力的Nitro隔离引擎,都是用Rust构建的。
但“更安全”不等于“绝对正确”。举一个最直观的例子:在C语言里,数组越界访问是一个后果完全不可预测的危险操作;换到Rust里,越界访问会让程序直接崩溃退出,这确实比C语言的“未定义行为”安全得多。可问题是,一段真正正确的代码,压根就不应该走到“越界访问”这一步——无论是崩溃还是继续跑下去,都说明代码本身有问题。
同样的道理,Rust的类型系统也无法保证程序算出来的结果就是开发者预期的那个结果,更无法保证程序不会意外泄露它能访问到的敏感数据。这些问题已经超出了编译器和类型系统的检查能力范围,需要另一套武器来解决——这就是Verus登场的地方。
Verus是一个开源的、面向Rust的自动化程序验证器。所谓“程序验证器”,指的是这样一类工具:你先给出一份关于代码应该如何运行的数学规约(specification),验证器再机械地检查代码在所有可能的输入下都满足这份规约。
举个例子:假设你写了一个优化过的二分查找函数,用来在一个有序数组里定位目标值。对应的规约可能是——如果函数成功返回了一个下标,那么数组里这个下标对应的元素必须正好等于目标值。而Verus要做的,就是对所有可能的数组和所有可能的目标值,机械验证这条规约始终成立。
这和传统测试有本质区别。测试只能挑几组具体的数组和目标值去跑一遍,很容易漏掉边界情况——比如目标值恰好是数组最后一个元素,或者目标值根本不在数组里。而形式化验证要求构造出一份严谨的数学证明,证明代码在任意输入下都不会违反规约。
在Verus这样的自动化验证器里,绝大部分繁琐、机械的证明步骤由工具自动完成,开发者只需要提供高层次的引导,比如搭建一个归纳证明的框架,或者补充一个循环不变式。而如今,就连这些高层引导,很多时候也已经可以交给AI来完成。
下面是一张简化的Verus工作流程示意图:

亚马逊是Rust基金会的创始成员之一,在Rust上的投入由来已久;再加上亚马逊在自动化推理领域已经积累了超过十年的经验,选择在Rust项目里引入Verus,几乎是水到渠成的事情。目前,亚马逊已经用Verus证明了Nitro隔离引擎所依赖的若干关键组件的正确性,也验证了内部其他一些关键基础设施。
Verus最与众不同的一个设计决策是:规约和证明都直接写在Rust源码里,语法风格也尽量贴近Rust本身。开发者不需要另外学一门规约语言,验证失败时看到的报错信息也是Rust风格、定位到具体源码行的。更重要的是,写代码的人往往就是最懂这段代码的人,让他们直接参与证明过程,比另外找一批专职的验证工程师要高效得多。
下面是一段示意性质的伪代码,模拟了Verus为二分查找函数标注前置/后置条件的方式(并非原文截图,仅用于说明思路):
// 示意代码:为二分查找函数标注Verus规约
verus! {
fn binary_search(arr: &[i32], target: i32) -> (result: Option<usize>)
requires
// 前置条件:数组必须是非降序排列的
forall|i: int, j: int| 0 <= i < j < arr.len() ==> arr[i] <= arr[j],
ensures
// 后置条件一:若返回了下标,该下标必须合法,且对应元素等于目标值
result matches Some(idx) ==> idx < arr.len() && arr[idx as int] == target,
// 后置条件二:若返回None,说明目标值确实不存在于数组中
result matches None ==> forall|i: int| 0 <= i < arr.len() ==> arr[i] != target,
{
// 具体实现省略
unimplemented!()
}
} // verus!
这里有两个细节值得注意:
第一,requires标注的是前置条件——本例中要求数组必须有序,这是二分查找算法成立的前提;ensures标注的是后置条件——不仅规定了返回Some(idx)时下标必须合法且对应元素匹配,还专门规定了返回None时目标值必须确实不在数组中。第二条后置条件容易被忽略,但它至关重要:如果没有这一条,一个永远返回None的“假二分查找”也能满足规约,因为它确实从不会返回错误的下标。
第二,requires、ensures、forall这类写法并不是合法的stable Rust语法,光靠标准rustc是编译不过的。Verus的做法是把这套规约语法包装进verus!这个宏里——这个宏由verus_builtin_macros等正式发布在crates.io上的proc-macro包提供。当项目只用普通stable Rust加Cargo编译、不经过Verus验证器本身时,这个宏会执行“幽灵代码擦除”(ghost erasure):把纯规约、纯证明的部分从展开结果里剥离掉,只保留真正会运行的可执行逻辑,最终生成一份合法、能被stable rustc正常编译的Rust代码。
这不是纸上谈兵,可以实际验证。只依赖verus_builtin和verus_builtin_macros这两个真实发布的crate(不装Verus验证器,只用普通stable rustc),写一个带requires/ensures的函数:
注:在cargo工程里通过cargo add添加verus_builtin和verus_builtin_macros两个crate依赖。
use verus_builtin_macros::verus;
use verus_builtin::*;
verus! {
fn add_one(x: u32) -> (y: u32)
requires
x < 100,
ensures
y == x + 1,
{
x + 1
}
} // verus!
fn main() {
let r = add_one(41);
println!("add_one(41) = {}", r);
// 故意用一个违反requires(x < 100)前置条件的输入调用函数,
// 看普通cargo build/run(未经过Verus验证器)会不会在运行时报错
let r2 = add_one(9999);
println!("add_one(9999) = {} (违反了requires,但仍正常返回)", r2);
}
用普通cargo build加stable rustc编译,完全没有任何报错,cargo run的输出是:
add_one(41) = 42
add_one(9999) = 10000 (违反了requires,但仍正常返回)
第二行是关键:传入9999明显违反了requires x < 100,但由于没有经过Verus验证器,代码在普通编译运行下完全没有把requires/ensures变成任何运行时检查——这两句规约被整段擦除了,而不是变成了一次assert!。翻一下verus_builtin_macros的源码也能看到确认这一点的逻辑:
#[cfg(not(verus_keep_ghost))]
pub(crate) fn cfg_erase() -> EraseGhost {
EraseGhost::EraseAll
}
也就是说,只要没有设置verus_keep_ghost这个cfg标志(普通cargo build默认就不会设置),宏在展开阶段就会把所有规约、证明相关的代码整体擦除,只留下真正会被编译执行的那部分逻辑。同一份源码,能被没有安装Verus验证器的项目通过标准Cargo正常消费,但前提是项目要显式依赖这些Verus配套crate——验证能力更像是一层可以按需叠加的“加分项”,而不是必须绕开的硬门槛。
Verus的另一个核心卖点是自动化程度高、反馈速度快。它背后依赖多种自动求解器(solver),负责把代码和规约转化出的证明义务自动“消化”掉。实际使用中,开发者写代码和证明后,通常能在一秒以内拿到反馈——这个速度足以支撑起交互式开发体验,比如在VS Code这类编辑器里像看到语法错误的红色波浪线一样,实时看到证明是否通过。
放到项目级别看,这种自动化的威力更明显:一些体量达到数千行代码加证明的复杂项目,Verus完成验证所需的时间,在过去一些早期自动化验证工具那里,可能只够验证单个函数。
这种“又快又省人力”的特性,不仅方便了人类开发者,也顺势打开了AI参与证明的大门——自动化程度越高,AI Agent需要自己动手补全的证明细节就越少,迭代速度自然也就越快。这或许也是形式化验证在AI辅助编程时代重新被重视的原因之一:过去写证明的门槛太高,现在人和AI可以一起把这道门槛降下来。
Rust的类型系统很强,但强到一定程度也会“束手束脚”——某些追求极致性能的写法,类型检查器无法证明其安全性,Rust因此专门开了一个口子,允许开发者显式标注unsafe代码块。这类代码依然必须遵守Rust对安全代码的所有约束,只是编译器不再替你机械检查,安全与否全靠开发者自己把关。
Verus在这里能帮上大忙:它可以为unsafe代码块提供数学层面的安全性证明,相当于把编译器放弃掉的机器检查能力,重新“找补”了回来。
并发场景是另一块难啃的骨头。Rust本身以“无畏并发”著称,类型系统会拦截掉很多其他语言在并发编程中常见的低级错误。Verus在这个基础上更进一步,让开发者不仅能证明并发代码是安全的,还能证明它在逻辑上是正确的。
一个典型场景是锁(lock)。并发执行往往需要锁来保证某个处理器线程独占访问一份共享数据。Verus允许开发者给锁附加一个“不变式”(invariant):任何人获得这把锁时拿到的数据一定满足这个不变式(比如某个数值永远是偶数),而在释放锁之前,必须证明数据依然满足这个不变式。更进一步,Verus还支持证明锁实现本身的正确性——这一点对Nitro隔离引擎这类依赖复杂自定义锁机制来换取高性能的系统尤其关键。

当然,任何验证工具的保证都不是凭空产生的,Verus也不例外。它的正确性最终依赖于几个层面:Verus工具本身是否可靠、开发者写的顶层规约是否真的表达了预期行为、对底层运行时(比如Rust标准库)所做的假设是否成立,以及把源码编译成可执行程序的整条工具链是否可信。这条“信任链”可以用下图简单表示:

亚马逊也提到,会在后续文章中详细介绍如何针对性地提升对这几个环节的信心,这也算是给读者提前挖了个坑。
除了在亚马逊内部落地,Verus也已经被不少开源项目拿去证明各自的关键属性:
Verus本身是一个完全免费、开源的项目,由学术界和产业界的一批研究者共同维护和推进。
从这篇文章能看出一个清晰的趋势:随着Rust在关键基础设施里的渗透越来越深,“类型安全”这一层保障正在变得不够用了。
亚马逊选择Verus的逻辑其实很朴素——规约和证明写在Rust源码里,语法贴近Rust,报错也是Rust风格,秒级反馈支持交互式开发,还能顺带啃下unsafe代码和并发这两块最难啃的骨头。这套组合拳,一方面照顾了人类开发者的学习成本,另一方面也天然适配了AI辅助编程的工作方式。
对于普通Rust开发者来说,短期内不一定人人都要给自己的代码写形式化证明,但了解Verus这类工具的存在和思路,至少提供了一种新的判断标准:什么样的代码值得投入成本去做“数学级别”的正确性保证——答案往往是那些一旦出错代价极高的关键路径,比如虚拟机隔离、密钥管理、支付链路这类系统。
参考资料
还在为写 Agent 框架频频死循环、上下文爆炸而束手无策?我的新专栏 《从0 开始构建 Agent Harness》 将带你:
扫描下方二维码,开启从 0 开始构建Agent Harness 的实战之旅。

还在为“复制粘贴喂AI”而烦恼?我的新专栏 《AI原生开发工作流实战》 将带你:
扫描下方二维码,开启你的AI原生开发之旅。

商务合作方式:撰稿、出书、培训、在线课程、合伙创业、咨询、广告合作。如有需求,请扫描下方公众号二维码,与我私信联系。
