LeanCIL 开源：用 Lean 4 证明 .NET CIL 属性
热点事件持续更新
LeanCIL 开源：用 Lean 4 证明 .NET CIL 属性
1 篇报道1 个报道来源2 小时前更新
先了解这件事
AI 综述
Nethermind 开源了 LeanCIL，它用 Lean 4 对编译后的 .NET 代码做形式化验证：从 C#、F# 等程序集提取 CIL，再针对显式指令模型检查证明，可证明任意长度循环的终止性、内存访问条件并给出反例。 支持范围限于整数运算、部分控制流与托管调用、无引用结构体、受检内存访问，以及整数、枚举、无引用结构体及其受支持整数向量构成的数组和 span（基于给定存储）、无引用数组分配、带类型的托管分派和部分运行时辅助函数与 SIMD 内建。一般类分配与虚分派、普通递归调用、异常处理、浮点运算和任意外部调用不在支持子集内。 使用需通过 elan 安装 Lean 4.35.0、.NET SDK 10.0.403（版本由 lean-toolchain 和 global.json 固定），代码以 Apache-2.0 或 MIT 双许可发布。
AI 根据报道生成 · 2 小时前更新
最新进展10月30日 18:29
LeanCIL：用 Lean 4 证明编译后 .NET 代码的性质报道时间线
沿着报道，了解事件的不同侧面。
10月30日
- Hacker NewsLeanCIL：用 Lean 4 证明编译后 .NET 代码的性质
LeanCIL 用 Lean 4 对编译后的 .NET 代码做形式化验证：从 C#、F# 等程序集提取 CIL，再针对显式指令模型检查证明，可证明任意长度循环的终止性、内存访问条件与反例。
本事件热度走势
还没有足够的连续观测数据，暂不绘制趋势。