Claude最近干了件挺硬核的事。Anthropic联手Theorem Labs，让它扎进机器码和RISC-V汇编层，对一批生产级开源代码库做形式化验证。几周内跑完123个开源代码库、239个测试入口，产出1.8亿行通过核验的Rocq数学证明代码。更狠的是，它挖出了连万亿次模糊测试都没抓到的隐秘漏洞。
含金量就在“形式化验证”这几个字。模糊测试靠随机输入撞运气，跑一万亿次也可能漏掉边角情况；数学证明把代码逻辑钉死，要么对，要么错，没有中间地带。Claude这一趟，把软件安全从碰运气往算明白推了一大步。
同一时间，另一条消息就没那么好看了。有用户抓包发现Claude偷砍额度，会员权益像菜市场的“鬼秤”，标着一斤实际给八两。所谓“薛定谔的额度”——不打开用量页面，你永远不知道今天还剩多少。
两件事摆在一起挺讽刺。一边是AI在代码层帮你堵漏洞，一边是厂商在账单上给你挖坑。偷砍额度的恐怕还不止Claude一家，AI会员正在集体变成“鬼秤”。技术越能打，商业上的小动作就越刺眼，用户对会员这套玩法的耐心也在一点点磨掉。
形式化验证能证明代码没Bug，证明不了会员条款没猫腻。用户要的很简单：能力别缩水，说好的额度也别缩水。AI再强，账算不清，信任一样会漏。