CSLib是面向计算机科学的形式化验证库（The Lean Computer Science Library），它把自动机、图灵机、逻辑、密码协议等经典理论用 Lean 语言严格写成可复用的库。本文带你用约 10 分钟，从零开始搭建第一个基于 CSLib 的 Lean 形式验证项目——无需深数学背景，照着敲命令即可跑通。

💡适合谁：想入门形式化方法、想验证算法正确性或学习 Lean 4 的工程师与研究生。

一、CSLib 是什么？为什么值得用 🎯

CSLib 的目标是让计算机科学的理论"可验证、可复用"。它提供三类能力：

与"自己从零写证明"不同，CSLib 把公共基础设施（标签迁移系统、关系工具、LTS 等）抽到 Cslib/Foundations/ 供各模块复用，让你站在巨人肩膀上。

核心入口文件是 Cslib/Init.lean，它统一配置了全库的默认 linter 与战术，几乎所有模块都会引入它。

二、准备环境：安装 Lean 4 工具链 ⏱️

CSLib 基于Lean 4与包管理工具Lake。推荐用官方的elan管理器自动锁定版本。

1. 安装elan（跨平台包管理器，会自动下载对应 toolchain）：

curl https://raw.githubusercontent.com/leanprover/elan/master/elan-init.sh -sSf | sh

2. 确认版本。CSLib 锁定在 lean-toolchain 文件指定的版本：

cat lean-toolchain # leanprover/lean4:v4.36.0-rc1

使用elan的好处：进入项目目录时它会自动切换到正确 toolchain，避免"版本对不上"的坑。

三、获取 CSLib 并构建 🚀

方式 A：把 CSLib 作为依赖引入你的项目（最常用）。在你的项目lakefile.toml中加入：

[[require]] name = "cslib" scope = "leanprover" rev = "main"

然后执行lake update cslib拉取依赖。想固定到某个稳定版本，可把rev换成对应的 release tag。

方式 B：克隆仓库直接体验（本文演示用）：

git clone https://gitcode.com/gh_mirrors/csl/cslib cd cslib lake build

首次构建会下载mathlib等依赖并编译整个库，请耐心等待几分钟。成功后你会得到两个目标库Cslib与测试库CslibTests（见 lakefile.toml 中的defaultTargets/testDriver配置）。

四、你的第一个验证：写个自动机并跑测试 ✍️

打开任意.lean文件，先引入 CSLib 的自动机模块，写一个"电梯"自动机（取自仓库测试用例 CslibTests/DFA.lean）：

import Cslib.Computability.Automata.DA.Basic open Cslib.Automata inductive Floor where | one | two deriving DecidableEq inductive Direction where | up | down deriving DecidableEq def elevator : DA Floor Direction where tr | .one, .up => .two | .one, .down => .one | .two, .up => .two | .two, .down => .one start := .one

DA是"确定性自动机"（Deterministic Acceptor），状态Floor、输入Direction、转移函数tr一一对应。接下来在 Lean 中补一个证明，验证"从一层按 up 会到二层"：

example : elevator.tr .one .up = .two := rfl

保存文件，运行：

lake build

若无报错，说明类型检查通过、证明被 Lean 内核接受——这就是"形式验证"的核心：机器替你确认逻辑无误。

五、跑通完整测试套件 🧪

CSLib 自带测试入口 CslibTests.lean，覆盖 DFA、λ演算、HML、电路等模块。一条命令全部执行：

lake test

它会编译CslibTests并运行其中的可执行测试。相关命令速查表：

命令细节参考 AGENTS.md 的 "Build & Validation Commands" 章节。

六、理解项目结构（10秒看懂）📁

cslib/ ├── Cslib/ # 主库源码 │ ├── Foundations/ # 公共基础：关系、LTS、单调性等 │ ├── Computability/ # 自动机 / 电路 / 图灵机 / 分布式 │ ├── Languages/ # 过程代数、λ演算等 │ ├── Logics/ # 模态、线性、命题逻辑 │ ├── Crypto/ # 密码原语与协议 │ └── Init.lean # 全局初始化（linter/战术） ├── CslibTests/ # 测试用例 ├── Cslib.lean # 汇总导入所有模块 └── lakefile.toml # 构建配置

• 想看"算法验证"的例子 → Cslib/Algorithms/
• 想看"分布式共识不可能性（FLP）"的完整证明 → Cslib/Computability/Distributed/FLP/
• 想看 CCS 进程代数实例（Milner 自动售货机）→ Cslib/Algorithms/CCS/VendingMachine.lean

每个子目录都配有 README，例如 Cslib/Computability/README.md 与 Cslib/Foundations/README.md 是了解设计理念的好入口。

七、新手常见问题（FAQ）❓

Q1：构建特别慢？首次会下载并编译mathlib等大型依赖，属于正常现象，后续增量构建会很快。

Q2：报"版本不匹配"错误？确认elan已按 lean-toolchain 切到正确 toolchain；或检查 lake-manifest.json 中的依赖是否完整拉取。

Q3：我的文件必须 importCslib.Init吗？在 CSLib 主库内是的，测试套件会检查这一约定（见 scripts/CheckInitImports.lean）。你自己的下游项目只需import Cslib即可。

Q4：想给 CSLib 提贡献？阅读 CONTRIBUTING.md，注意 PR 标题需以feat/fix/doc/...等前缀开头。

八、下一步学习路线 🗺️

1. 跑通示例：在CslibTests/里挑一个感兴趣的测试文件，读懂它的证明。
2. 换模块练手：从 CslibTests/DFA.lean 扩展到电路、λ演算等其它模块。
3. 写自己的证明：把一个小算法（如排序）的正确性写成 Lean 定理并用 CSLib 工具验证。

🎉 恭喜！你已搭好一个可复用的 Lean 形式验证项目，并能用 CSLib 持续验证你的算法与系统。祝验证愉快！

相关文档：README.md · AGENTS.md · CONTRIBUTING.md