LeanCIL – 使用 Lean 4 验证编译后的 .NET 代码属性

LeanCIL 利用 Lean 4 验证编译后的 .NET 代码属性，支持从 C#、F# 等语言提取 CIL 并验证证明，可证明输入满足合同、循环终止、内存访问条件等，支持组合已证明的方法合同，不展开辅助体。LeanCIL 支持 4.35.0 版本，通过 elan 和 .NET SDK 10.0.403 安装。