thiagomassensini/c2_lean
GitHub: thiagomassensini/c2_lean
使用 Lean 4 定理证明器对 C2 框架核心架构进行形式化建模与数学验证的研究项目。
Stars: 0 | Forks: 0
# LeanC2
使用 Lean 4 + Mathlib 对 C2 框架进行形式化，重点关注离轴
链、continuation 接口、数字证书钩子，以及连接到 C2 -> RH 包的公共
端点。
## 构建
```
lake exe cache get
lake build
```
## 快速结构
- `LeanC2/` 包含主要的形式化图谱。
- `LeanC2/PublicAPI.lean` 暴露了项目的公共接口。
- `LeanC2/Numerical/Generated/` 包含从
canonical 验证流程使用的外部证书生成的 Lean 工件。
## 参考文献
- 架构：`c2_lean_architecture.md`
- 遗留复用映射：`legacy_reuse_map.md`
- 保留的遗留代码：`Antigo_Lean_C2/`
## 引用
引用和发布元数据在 `CITATION.cff`、`.zenodo.json`
和 `ZENODO_RELEASE_2026-05-06.1.md` 中提供。
标签：C2 -> RH包, C2架构, C2框架, Lean 4, Mathlib, Runtime Enforcement, 云安全监控, 代码生成, 公共API, 安全学习资源, 定理证明, 延续接口, 形式化数学, 形式化验证, 数值计算接口, 数值证书, 模块化开发, 渗透测试工具, 离轴链, 符号验证, 编译器技术, 网络安全, 软件架构, 隐私保护, 静态分析