Rosu 实验室发布 KIT：让编码代理生成代码即自动形式化验证
LingmingZhang · x · 2026-10-22
Grigore Rosu 的研究实验室发布 KIT，让 AI 编码代理在生成代码的同时自动做形式化验证，每个结论都有编程语言的数学真值背书，目前已可用于 Python 和 Solidity/EVM，Rust、C、JavaScript 等在支持计划中。
工作方式：
- 从代码中提取意图，生成形式化 spec（基于 K 框架），再由 Prover 证明并审计证明
- 安装即用：claude plugin marketplace add nlp-research-rosu/kit-plugin 后 claude plugin install kit@kit-plugin，同时支持 Claude Code、Codex 桌面端与 VS Code
- 使用时在 agent 里选中安全关键代码，按 P0–P3 严重度排序验证关注点，输出哪些性质成立
团队接下来将在大量开源系统上运行 KIT 找真实 bug，正在征集目标库。
「编程与Agent」频道最新
- swyx 称 Opus 5.5 是最佳工时估算模型，开发者反驳：审查时间才是瓶颈 — petrusenko_max · 2026-10-23
- 针对 LiteLLM 供应链事故,作者发布 6 套 Agent 网络防御工具包 — alvelda · 2026-10-23
- Agent Field Kit 发布免费工具箱，应对 LLM 增强型攻击者 — alvelda · 2026-10-23
- LiteLLM 供应链投毒与 Railway 凭据泄露：10·21 攻击完整时间线与应急处置 — alvelda · 2026-10-23
- AI 每日实验规划 agent:一个 prompt 帮科学家省去跑腿确认试剂库存 — nlarusstone · 2026-10-23
- 两台 £300 骁龙迷你 PC 无 GPU 跑 Qwen3.8 Flash Next，实测 46 tok/s — WorldlyAd7946 · 2026-10-22