Repolode
提交项目
NethermindEth

NethermindEth/LeanCIL

基于 Lean 4 的形式化验证框架，可对 C#、F# 等 .NET 语言编译出的 CIL 字节码进行机器可检查的正确性与内存安全证明。

在 GitHub 查看
Star
110
Fork
3
未关闭 Issue
21
最近提交
前天

这是什么？

LeanCIL 从编译好的 .NET 程序集中提取 Common Intermediate Language（CIL），并依据对这些指令的显式模型，用 Lean 4 检查证明。它可以证明满足契约的所有输入都具有某种结果，证明循环终止，检查内存访问条件，或给出错误实现的反例。已证明的方法契约可以直接组合使用，无需展开辅助函数的实现。

命令行工具提供列出方法签名、提取目标方法及其可达调用、检查提取产物、以及对指定定理进行内核重放和公理审计等功能。验证通过后会生成 verified.json 报告，并与程序集的 SHA-256 绑定。应用可以把规约和证明放在独立的 Lean 项目中，并固定依赖 LeanCIL。

当前支持的子集包括整数运算、部分控制流、托管方法调用、无引用类型的结构体，以及基于已提供存储的数组和 Span。浮点运算、通用类对象分配、虚方法分派、普通递归和异常处理不在模型范围内。项目并不声称完整验证 CLR 或 JIT 的行为。

核心功能

  • 01借助 Lean 4 证明，对满足契约的所有输入验证函数性质。
  • 02从编译后的 C#、F# 等 .NET 程序集中提取并校验 CIL。
  • 03在带检查的内存模型中验证内存访问、边界、初始化和对齐。
  • 04无需展开辅助方法实现，即可组合已证明的方法契约。
  • 05生成与程序集 SHA-256 绑定的 verified.json 验证报告。

适用场景

  • 证明 .NET 中的算术或缓冲区例程对所有输入都行为正确。
  • 验证对 Span 的循环会终止，且可写区域之外的内存保持不变。
  • 为不符合规约的实现找出反例。

快速上手

  1. 1

    通过 elan 安装 Lean 4.35.0，并安装 .NET SDK 10.0.403

  2. 2

    在代码仓库目录中构建 Lean 项目

    lake build
  3. 3

    将 Extractor 打包为本地 NuGet 包

    dotnet pack Extractor -c Release -o artifacts/packages
  4. 4

    从本地包全局安装 leancil 工具

    dotnet tool install --global Nethermind.LeanCIL --add-source artifacts/packages --version 0.1.0

使用前须知

  • 仅支持受限的 CIL 子集；通用类分配、虚分派、异常处理程序和浮点运算不受支持。
  • 需要同时安装 Lean 4 工具链和 .NET SDK，并使用指定的固定版本。
  • 项目处于早期阶段，版本为 0.1.0，社区规模较小。

标签

#formal-verification#lean4#dotnet#cil#theorem-proving#memory-safety

常见问题

LeanCIL 是什么？
基于 Lean 4 的形式化验证框架，可对 C#、F# 等 .NET 语言编译出的 CIL 字节码进行机器可检查的正确性与内存安全证明。 LeanCIL 从编译好的 .NET 程序集中提取 Common Intermediate Language（CIL），并依据对这些指令的显式模型，用 Lean 4 检查证明。它可以证明满足契约的所有输入都具有某种结果，证明循环终止，检查内存访问条件，或给出错误实现的反例。已证明的方法契约可以直接组合使用，无需展开辅助函数的实现。
LeanCIL 可以免费使用吗？用的什么许可证？
LeanCIL 以 Other 许可证开源。用于商业产品前，请先确认许可证条款。
LeanCIL 还在维护吗？
活跃维护中。LeanCIL 最近一次提交是在 2026年11月5日。
LeanCIL 适合用来做什么？
证明 .NET 中的算术或缓冲区例程对所有输入都行为正确。 验证对 Span 的循环会终止，且可写区域之外的内存保持不变。 为不符合规约的实现找出反例。
LeanCIL 怎么安装和运行？
通过 elan 安装 Lean 4.35.0，并安装 .NET SDK 10.0.403 在代码仓库目录中构建 Lean 项目: lake build 将 Extractor 打包为本地 NuGet 包: dotnet pack Extractor -c Release -o artifacts/packages 从本地包全局安装 leancil 工具: dotnet tool install --global Nethermind.LeanCIL --add-source artifacts/packages --version 0.1.0
在哪里获取 LeanCIL？
源代码和安装说明在 GitHub 上：https://github.com/NethermindEth/LeanCIL

概要由 AI 根据项目 README 生成；GitHub 数据每日更新。

相关项目