Cursor 开始往 Claude Code 的市场里发插件了，最新那个让 agent 对你仓库里最难的部分做形式化验证
cursor/plugins 这个仓库周末上了 GitHub 日榜，一天 15 次提交，12705 颗星，值得注意的不是任何一个插件。是 .claude-plugin/marketplace.json 这个文件，所有者 Cursor，联系邮箱 [email protected]，它把 Cursor 的两个插件挂进了 Claude Code 的插件市场：origin-apps，用来在 Cursor Origin API 上开发；还有 pstack，源路径是 harness/pstack/claude-code。那个目录 10 月 16 日第一次提交，PR 标题是从生成的目录树把 pstack 装进 Claude Code，此后十二次提交，最新一次在周六晚上。Android 上周把自己的 skills 发进了 Claude Code 和 Codex 的市场。Cursor 这么做是另一种信号，因为 Cursor 卖的是竞争的那个 harness。
仓库本身是 Cursor 的官方插件规范，加大约十七个第一方插件和五十五个第三方集成，每个是一个带 .cursor-plugin/plugin.json 清单的目录。第一方列表读起来像今年 agent 模式的目录：continual-learning 用高信号要点对 AGENTS.md 做增量的、由对话记录驱动的记忆更新，thermos 是带并行子 agent 的热核级分支审查，ralph-loop 是 Ralph Wiggum 式迭代循环，orchestrate 把大任务分发给并行云端 agent，有规划者、执行者、验证者和结构化交接，advisor 在重大决策前咨询一个更强的模型，cli-for-agent 是一份让 agent 能可靠运行 CLI 的设计模式。这些全是文本文件。规范才是产品，插件是一家厂商认为规范该承载什么的示例。
该读的是周六合并的那个 PR。709 号给 pstack 加了 /create-formal-verification-skill，正文由 Cursor 的 agent 写，开头是：测试只检查有人想到要写的情况；竞态、重试、状态机、解析器和不安全代码常常栽在没人写过的那种情况上。这个技能选仓库里最强的目标，不是最容易验证的那个；挑一个验证工具并说明理由；验证一条性质，并在故意弄坏的代码变体上展示这条性质失败；然后写一个项目本地的技能，让下一个 agent 能判断某次改动是否碰到了被验证的代码，一条命令重跑检查，并分清真 bug 和建模错误。接着它在一次会破坏该性质的临时改动上照自己新写的技能走一遍，确认检查能抓住，再把改动丢掉。它不会为了通过而削弱性质或模型。周六晚上的一次后续提交把形式化验证加进了 pstack 的安装选项。
把它和这周的其他条目放在一起看，方向很明显。Sphinx 在 push 时卡人的理解。Claude Code 团队的审稿帖和 Postgres 19 推迟说审查是瓶颈。vLLM 说 agent 写的内核跑赢了审稿人，想要自动验证。Cursor 的回答，以一个 markdown 技能的形式发进 Anthropic 的市场：让 agent 给最伤人的那一条不变量造一个验证器，然后作为技能留给下一个 agent。拥有编辑器的 harness 正通过对手的包管理器分发自己的验证习惯，因为技能文件现在是分发单位，harness 只是它运行的地方。
链接：https://github.com/cursor/plugins ，https://github.com/cursor/plugins/pull/709 ，https://github.com/cursor/plugins/blob/main/.claude-plugin/marketplace.json
← 返回所有文章
仓库本身是 Cursor 的官方插件规范，加大约十七个第一方插件和五十五个第三方集成，每个是一个带 .cursor-plugin/plugin.json 清单的目录。第一方列表读起来像今年 agent 模式的目录：continual-learning 用高信号要点对 AGENTS.md 做增量的、由对话记录驱动的记忆更新，thermos 是带并行子 agent 的热核级分支审查，ralph-loop 是 Ralph Wiggum 式迭代循环，orchestrate 把大任务分发给并行云端 agent，有规划者、执行者、验证者和结构化交接，advisor 在重大决策前咨询一个更强的模型，cli-for-agent 是一份让 agent 能可靠运行 CLI 的设计模式。这些全是文本文件。规范才是产品，插件是一家厂商认为规范该承载什么的示例。
该读的是周六合并的那个 PR。709 号给 pstack 加了 /create-formal-verification-skill，正文由 Cursor 的 agent 写，开头是：测试只检查有人想到要写的情况；竞态、重试、状态机、解析器和不安全代码常常栽在没人写过的那种情况上。这个技能选仓库里最强的目标，不是最容易验证的那个；挑一个验证工具并说明理由；验证一条性质，并在故意弄坏的代码变体上展示这条性质失败；然后写一个项目本地的技能，让下一个 agent 能判断某次改动是否碰到了被验证的代码，一条命令重跑检查，并分清真 bug 和建模错误。接着它在一次会破坏该性质的临时改动上照自己新写的技能走一遍，确认检查能抓住，再把改动丢掉。它不会为了通过而削弱性质或模型。周六晚上的一次后续提交把形式化验证加进了 pstack 的安装选项。
把它和这周的其他条目放在一起看，方向很明显。Sphinx 在 push 时卡人的理解。Claude Code 团队的审稿帖和 Postgres 19 推迟说审查是瓶颈。vLLM 说 agent 写的内核跑赢了审稿人，想要自动验证。Cursor 的回答，以一个 markdown 技能的形式发进 Anthropic 的市场：让 agent 给最伤人的那一条不变量造一个验证器，然后作为技能留给下一个 agent。拥有编辑器的 harness 正通过对手的包管理器分发自己的验证习惯，因为技能文件现在是分发单位，harness 只是它运行的地方。
链接：https://github.com/cursor/plugins ，https://github.com/cursor/plugins/pull/709 ，https://github.com/cursor/plugins/blob/main/.claude-plugin/marketplace.json
评论