Meta公开可在CPU运行的Lean GPU内核安全核验组件

Meta的lean_kernel_verify（LKV）把GPU内核的编译器IR转为简化KIR，再由Lean 4在具体case输入上检查越界、地址回绕、缺失/重复写入、屏障协议及部分TMEM复用约束。29日首次实质源码包含Lean求值/规范层、KIR转换、命令入口、原生Agent Skill和测试，采用MIT许可。Skill指导编程Agent核对内核revision及修复，案例要求检查Q/K空段、head和滑动窗口等注意力内核边界。 当前可从公开clone在Linux、Lean 4.34及Python>=3.10环境运行scripts/lkv.py check与对应Lean/KIR测试，不需要GPU。但run仍通过内部monorepo的Buck2构建前端，export仍读内部内核源码，公开clone会明确报错。结论只覆盖case文件的具体输入，不检查数值、性能，也不保证一般性的无race或无死锁。本条收录可独立使用的核验组件，不宣称整个自动前端管线已经可独立部署。