SZLHOLDINGS/szl-cookbook-source

szl-cookbook源仓库镜像，用于szl-cookbook治理配方库。包含YAML配方定义、模式文档和测试夹具。配方是可执行的治理程序，用于：DSSE收据签发、SLSA来源生成、OTel跨度发射和Lean定理验证。可通过[szl-cookbook-runner空间](https://huggingface.co/spaces/SZLHOLDINGS/szl-cookbook-runner)进行实时执行。This is a mirror of the szl-cookbook source repository, dedicated to managing the szl-cookbook governance recipe library. It includes YAML recipe definitions, schema documentation, and test fixtures. The recipes are executable governance programs that support: DSSE receipt issuance, SLSA provenance generation, OTel span emission, and Lean theorem verification. Real-time execution is available via the [szl-cookbook-runner Space](https://huggingface.co/spaces/SZLHOLDINGS/szl-cookbook-runner).

原始信息汇总

数据集概述：szl-cookbook-source

• 数据集名称：szl-cookbook-source
• 提供者：SZLHOLDINGS
• 任务：其他（Other）
• 语言：英语（English）
• 数据集规模：n<1K
• 许可证：Apache-2.0

数据集描述

该数据集是 szl-cookbook 治理配方库的源代码仓库镜像，包含 YAML 配方定义、模式文档和测试夹具。

配方是可执行的治理程序，涉及以下功能：

• DSSE 收据签发
• SLSA 来源生成
• OTel 跨度发射
• Lean 定理验证
• 通过 szl-cookbook-runner space 进行实时执行

标签

包含以下标签：formal-verification、lean4、mathlib、dsse、governance、agentic-ai 等。

状态（截至2026-05-30）

指标	数值
Lean 声明数	626
Lean 公理数	15（14个唯一）
Lean sorries 数	189（138基线 + 51 Putnam）
锚定公式数	40
Kernel green	Mathlib 4.13.0
HF Spaces 数	27
HF Datasets 数	31
Zenodo DOIs	6个发布 + 1个概念别名
Putnam 2025 覆盖率	10/12 结构，4/12 GREEN（Lean已证明）

交叉引用

• 论文：Ouroboros Thesis v18 · DOI 10.5281/zenodo.20434276
• Lean 伴侣：lutar-lean · DOI 10.5281/zenodo.20424992
• 收据：MCP 服务器 · szlholdings-mcp-receipts-server.hf.space
• 测试结果：SZLHOLDINGS/test-results
• 目录：SZLHOLDINGS on HuggingFace
• 源码：szl-cookbook-source on GitHub

来源信息

字段	值
生态系统阶段	generated-mirror
生态系统阶段矩阵	SZLHOLDINGS/szl-anatomy → Stage Matrix
MCP 网关	szlholdings-mcp-receipts-server.hf.space
Doctrine	v7 — 无营销语言，每个数字可解析到CI日志或Zenodo DOI
论文 DOI	10.5281/zenodo.20434276
Lean 伴侣 DOI	10.5281/zenodo.20424992
作者	Stephen Paul Lutar Jr. · ORCID 0009-0001-0110-4173

使用统计

• 上月下载量：226
• 总文件大小：7.12 MB

搜集汇总

数据集介绍

构建方式

szl-cookbook-source数据集作为治理配方库的源镜像而构建，其核心内容涵盖YAML格式的配方定义、配套的架构文档以及测试夹具。该数据集通过系统化整合来自Lean定理证明器、DSSE收据签发、SLSA溯源生成及OTel跨度发射等领域的可执行治理流程而形成，每一则配方均映射至相应的自动化执行程序。数据集的版本控制与更新机制依托于GitHub仓库的持续集成流水线，并借助Zenodo实现持久化标识与版本固化，从而确保数据的可追溯性与可复现性。

使用方法

用户可通过HuggingFace上的szl-cookbook-runner空间直接执行数据集中的配方，该空间作为Rust MCP服务器实时运行。具体而言，用户能够针对DSSE收据签发、SLSA溯源生成、OTel跨度发射及Lean定理验证等任务调用相应的配方定义，并实时查看执行结果与验证状态。数据集的每个版本均通过Zenodo DOI进行标识，用户可通过指定DOI引用特定版本的数据集内容。此外，数据集提供了完整的架构文档与测试夹具，支持用户在此基础上进行二次开发与集成，以扩展至更广泛的形式化验证场景。

背景与挑战

背景概述

szl-cookbook-source数据集由Stephen Paul Lutar Jr.于2025年创建，依托SZLHOLDINGS组织发布，核心研究问题在于通过可执行治理程序（Recipes）实现形式化验证与软件供应链安全的深度整合。该数据集镜像了Lean4定理证明器与Mathlib数学库的治理流程，包含626个Lean声明、40个锚定公式及189个待证明缺口（sorries），覆盖DSSE收据签发、SLSA溯源生成、OTel跨度发射等关键安全治理环节。作为Ouroboros论文（DOI:10.5281/zenodo.20434276）的配套数据资源，它为Agentic AI环境下的可验证计算提供了基础框架，推动了形式化方法在现实系统治理中的落地应用。

当前挑战

该数据集面临的领域挑战在于如何弥合形式化验证与复杂系统治理之间的鸿沟。一方面，传统治理流程缺乏数学保证，而Lean证明的高门槛（如189个sorries需逐步消解）限制了其大规模部署。另一方面，构建过程中需协调多源异构数据（YAML配方、Lean代码、CI日志）的版本一致性与可溯源性，例如确保每个数字可解析至CI日志或Zenodo DOI的Doctrine v7要求。此外，在Putnam竞赛覆盖场景中，仅4/12问题获得完全Lean验证，凸显了将非形式化数学推理自动化编码为可执行治理程序的持续挑战。

常用场景

经典使用场景

szl-cookbook-source数据集是面向形式化验证与治理自动化领域的一份独特资源，其核心价值在于将数学证明与可执行治理流程相融合。该数据集最经典的使用场景是作为“可执行治理配方库”，研究人员和工程师可以通过YAML配方定义、模式文档及测试夹具，驱动DSSE收据签发、SLSA溯源生成、OpenTelemetry跨度发射以及Lean定理验证等治理流水线的自动化执行。借助该数据集，用户能够以数学严谨性为基，构建从代码到合规的可审计闭环，从而在DevOps与形式化验证的交汇处开辟新的实践范式。

解决学术问题

该数据集针对软件供应链安全与治理领域长期存在的“形式化验证与实际部署相割裂”这一核心矛盾，提供了一套可复现、可验证的解决方案。它实现了从Lean定理证明器到具体治理程序的端到端映射，使得每一项治理操作都能追溯到经过数学验证的锚定公式和Lean声明。通过将40个锚定公式、626条Lean声明以及189个待补全证明（sorries）编织进统一的配方库，该数据集为研究社区提供了评估形式化验证在真实治理场景中覆盖度与成熟度的基准，推动了可验证可信计算基础设施的学术探索。

实际应用

在实际应用中，该数据集支撑起一套完整的“可执行治理生态系统”，特别适用于需要高合规性和可审计性的金融科技、医疗数据和政务系统等领域。企业可以通过MCP（Model Context Protocol）服务器实时调用配方库中的治理流程，自动生成DSSE收据和SLSA溯源凭证，从而满足供应链安全等级要求。此外，该数据集还支持Lean证明状态的可视化追踪，使得运维人员能够直观地监控治理流程的数学完备性，为自动化合规审计和风险管控提供了前所未有的技术手段。

数据集最近研究

最新研究方向

该数据集聚焦于将形式化验证与自动化治理协议相融合的前沿方向，通过Lean4定理证明器与DSSE、SLSA等供应链安全标准的深度集成，推动数学证明与软件供应链可审计性的交叉研究。其最新进展体现在对2025年Putnam数学竞赛12道题目中10道结构的覆盖，并成功以Lean内核绿色验证了4道完整证明（A1、A5、B4、B6），标志着智能体驱动的形式化推理在竞赛级数学问题上的重大突破。此外，结合MCP服务器与RAE-1协议的实施，数据集为构建可执行的治理食谱库提供了可复现的基础设施，其影响力延伸至代理型AI系统的安全验证与数学定理的自动化证明领域。