AI 形式验证工具发现 Redis 与 Valkey 的可复现漏洞

Litmus 团队用 AI 驱动的形式验证工具检查 Redis 与 Valkey，发现多个可复现的真实 bug，包括数个内存安全问题，目前正在协调披露。团队先提取代码意图，再形式化属性与不变量并寻找、验证反例，其中一条仅 23 个字符的命令可冻结整台 Redis 服务器。