给形式化方法的人更多细节——正在发生的是 Claude 在做类似这样的事情：

给形式化方法领域的读者更详细的说明——目前的情况是，Claude 正在做如下工作：

1. 针对程序中某个复杂的有限状态机或易发生竞态的代码部分，构建其模型。
2. 在该模型中寻找反例。这些反例被认为是潜在的缺陷。
3. 重现这些缺陷。
4. 修复代码中的这些缺陷。

并不是说整个代码库都经过了形式化验证（至少目前还没有！），而是对代码中最棘手的部分进行建模、检查是否存在反例，并予以修复。