零手写 spec:Hydro 框架用 Verus 自动验证分布式系统交换律
ShadajL · x · 2026-09-18
开发者 Shadaj L 宣布 hydrolang 合入了基于 Conor Power 博士论文成果的新特性:为分布式流处理框架 Hydro 的交换律(commutativity)标注提供 Verus 机器检查证明,替代手写 manualproof!。关键设计:
- 用户完全不用写断言——证明义务由宏从实际闭包体自动生成;
- 证明按算子形状定制:fold/reduce 要求两种顺序下最终累加器相等;map 要求捕获状态相等且输出多重集相等(可捕捉暴露顺序的输出如运行累计值);filter 要求决策一致与保留多重集相等;
- 证明通过通用属性机制接入 q!,保证对下游任意效果重排不可观察。
这是把形式验证工程化落地到数据流框架的典型案例,论文基础表明无需手写 spec 也能形式化验证分布式系统。
「编程与Agent」频道最新
- Pictify MCP Server:让 AI 助手从 HTML 生成图、GIF 与 PDF — modelcontextprotocol · 2026-09-18
- convalytics:通过 MCP 为 Convex 应用提供只读分析查询 — modelcontextprotocol · 2026-09-18
- 开发者用 Codex 托管 Slack 回复，附完整提示词与自改进机制 — alex_frantic · 2026-09-18
- 开发者用 Codex 起草 Slack 回复:无需反馈即可自我调优 — alex_frantic · 2026-09-18
- 八个月迭代 ATLAS:不动权重把小模型推向接近前沿水平的编码系统 — itigges22 · 2026-09-18
- 新浏览器 API 提案：应用内直接验证邮箱，无需跳出跳转收件箱 — philnash · 2026-09-18