今日速览

今天不是单一大厂发布带节奏，而是工程侧的细节更有意思。HN 上有形式化证明、HyperCard 式创作工具；GitHub Trending 里 agent 浏览器和自托管 CMS 很醒目；V2EX 则把 AI 编程工具的落地问题讲得很直接。Dev Digest 编辑今天选了 10 条，质量够，不需要硬凑。

条目

  1. We have proof automation now · Hacker News

    Adam Langley 这篇文章围绕 zstd 与 Lean 的证明自动化展开，核心不是炫形式化方法，而是说明工具链开始能处理更贴近真实系统代码的证明工作。对工程团队来说，这类进展值得关注：安全关键路径、压缩库、密码学和编译器优化，未来可能不只靠测试和代码审查兜底。它也提醒我们，证明自动化要真正有用，必须嵌进普通开发流程，而不是停留在研究 demo。

  2. Decker, a platform that builds on the legacy of HyperCard and classic macOS · Hacker News

    Decker 是一个继承 HyperCard 和经典 macOS 气质的创作平台，强调小工具、文档、交互和可分享性。它有点逆潮流：不是把所有东西塞进重型 Web app，而是让个人和小团队快速做出可用的交互对象。对今天的开发者来说，这种轻量创作环境很值得重新看，因为 AI 生成代码越容易，越需要一个能快速验证想法的低摩擦界面。

  3. An Inside Look at the Relay Market Powering Token Resellers and Fraud · Simon Willison

    Simon Willison 摘评了 LLM token 转售和中转市场的调查，里面涉及免费试用滥用、未保护机器人、被盗卡和代理聚合。中文读者应该会觉得这事不陌生，但值得严肃对待的是：一旦你的公开 AI endpoint 没有限额、鉴权和预算上限，它就可能变成别人套利链条的一环。便宜 token 背后不只是灰产价格战，还有数据、合规和账单风险。

  4. citrolabs/ego-lite · GitHub Trending

    ego-lite 的定位是给 AI agent 跑 Web 自动化的高速浏览器，并支持共享已登录浏览器状态。这个方向非常现实：很多 agent 任务卡在登录态、浏览器隔离和用户工作流打扰上。团队在评估这类工具时，除了速度，也要看会话边界、凭据隔离、审计记录和失败恢复，否则“让 agent 代点几下”很快会变成权限管理问题。

  5. CoreBunch/Instatic · GitHub Trending

    Instatic 把自己定位成 Webflow、Framer 和 WordPress 的开源替代，强调自托管、可视化 CMS 和输出静态页面。它值得进入今天列表，是因为 AI 辅助建站会放大“生成后怎么维护”的问题。对企业和个人站点来说，能否把页面、角色、插件、数据和部署都纳入可控系统，比一次生成一个漂亮页面更重要。

  6. 不跳就锁——用心率广播实现人走锁屏 · V2EX

    这条 V2EX 讨论很有工程味：用心率广播判断人是否离开，从而触发锁屏。它不是大项目，但把可穿戴设备、桌面安全和自动化串了起来。对远程办公和共享办公环境来说，这类小自动化有实际价值，前提是误判、隐私和手动覆盖都要设计清楚。

  7. Code Agent 的 edit 工具有没有在生成阶段就防幻觉的方案？ · V2EX

    这条讨论问的是 AI code agent 的 edit 工具能否在生成阶段就减少幻觉，而不是事后检查。这个问题很关键：post-edit lint 和测试当然必要，但如果编辑器接口本身不能约束目标文件、上下文范围和补丁格式，错误会更早进入工作区。更稳的方向是结构化 patch、上下文校验、最小 diff 和失败可回滚，而不是让模型自由写整段文件。

  8. Opus5が思考が浅いように感じる問題への対策 · Zenn

    这篇 Zenn 文章讨论使用 Opus 5 时“思考变浅”的体感和应对方式。它有参考价值，因为模型升级后不一定所有旧提示词都继续有效，尤其是依赖长上下文、规则列表和隐含约束的工作流。中文团队如果已经把 Claude 或同类模型接入开发流程，应该把提示词、上下文模板和评测样例当成版本化资产维护。

  9. MCP仕様が明日アップデート、7月28日版MCPからはステートレスな接続が正式仕様に · Publickey

    Publickey 报道 MCP 7月28日版规格将把 stateless 连接纳入正式规格，GitHub MCP server 也已表态支持。MCP 正在从“能连上工具”进入“怎么稳定连、怎么扩展、怎么跨服务运维”的阶段。对做内部 agent 平台的团队来说，连接状态、会话恢复、认证和多客户端兼容会越来越重要。

  10. Introducing Claude Opus 5 · Anthropic

    Anthropic 官方的 Opus 5 发布仍然值得放进今天列表，因为社区讨论正在从能力榜单转向安全、prompt injection 和长期任务表现。官方材料强调复杂推理、编码和主动性，但工程团队更应该同步看系统卡、价格、速率限制和工具调用行为。模型发布不是采购结论，只是评估开始。

编者按

今天选了 10 条，源分布为 HN 2、GitHub Trending 2、Simon Willison 1、V2EX 2、Zenn 1、Publickey 1、Anthropic 1。所有指定来源今日均可访问；V2EX 已跳过广告、情感和非工程向热门帖。Dev Digest 编辑建议优先读 Simon 的 token 转售调查、MCP stateless 更新和 Code Agent edit 讨论：它们分别对应成本滥用、agent 基础协议和自动化写代码的实际边界。