Math, Inc. 发布从 C 源码推导的 Linux WireGuard 握手可执行 Lean 形式化模型

Math, Inc. 发布从 C 源码推导出 Linux 内核 WireGuard 握手协议的可执行 Lean 模型，旨在以机器可检验的方式证明代码正确性。该项目采用 specification engineering（规格工程）与语义抽象分层，团队认为这比直接在机器码层面证明更适合规模化自动验证。