a11oy-verifiable-corpus

a11oy可验证语料库是一个旨在提供完全可独立验证的数据集，遵循“无需信任，自行验证”的核心原则。它由SZL Holdings的a11oy系统生成，以仅追加、内容寻址的方式发布，确保历史记录的完整性和幂等性。数据集包含三个主要部分，均以NDJSON格式存储，并通过`head.json`文件维护链状态：1. 收据部分：包含完整的数字签名收据（DSSE信封）以及验证所需的所有密码学材料，支持两种真实的签名方案（ECDSA-P256-DSSE-PAE签名和Sigstore无密钥收据），并提供了详细的自行验证步骤和示例代码。2. 定理部分：嵌入了从lutar-lean仓库获取的、经Lean内核验证的定理列表，内容逐字节复制，每条记录包含原始Markdown文件内容、SHA256哈希、摘要（含计数和源文件自身声明的诚实标记）以及来源URL，用户可通过克隆源仓库并运行构建来独立验证。3. 公式部分：包含了a11oy规范公式注册表中的每个公式，记录包含公式名称、可调用函数及其证明状态，其中证明状态是从注册表中逐字复制的，反映了Lean内核和Doctrine v11诚实表面所定义的状态（如已证明、公理门控、假设、实数、猜想）。数据集遵循a11oy的诚实原则，明确区分条件性证明与无条件证明，并排除了所有非密码学签名的演示级工件。其数据规模较小（小于1K），适用于密码学证明、形式化验证、出处追溯、数字签名验证等任务，采用Apache-2.0许可证发布。The a11oy Verifiable Corpus is a dataset designed to provide fully independently verifiable content, adhering to the core principle of "trust nothing, verify everything". It is generated by the a11oy system under SZL Holdings, and released in an append-only, content-addressable manner to ensure the integrity and idempotency of historical records. The dataset consists of three main components, all stored in NDJSON format, with the chain state maintained via the `head.json` file: 1. Receipts Component: Contains complete digitally signed receipts (DSSE envelopes) and all cryptographic materials required for verification, supporting two genuine signature schemes (ECDSA-P256-DSSE-PAE signatures and Sigstore keyless receipts), and provides detailed step-by-step self-verification instructions and sample code. 2. Theorems Component: Embeds a list of theorems verified by the Lean kernel, sourced from the lutar-lean repository with content copied byte-for-byte. Each record includes the original Markdown file content, SHA256 hash, metadata (including counts and the honesty marker declared by the source file itself), and the source URL. Users can independently verify by cloning the source repository and running the build process. 3. Formulas Component: Contains every formula from the a11oy canonical formula registry. Each record includes the formula name, callable functions, and its proof status. The proof status is copied verbatim from the registry, reflecting the state as defined by the Lean kernel and Doctrine v11's honest surface (e.g., proven, axiom-gated, assumed, real numbers, conjectured). The dataset adheres to the a11oy honesty principle, explicitly distinguishes between conditional and unconditional proofs, and excludes all non-cryptographically signed demo-level artifacts. It is small in scale (fewer than 1,000 entries), suitable for tasks such as cryptographic proof, formal verification, provenance tracking, and digital signature verification, and is released under the Apache-2.0 license.

原始信息汇总

数据集概述

a11oy Verifiable Corpus 是一个专注于可验证性的数据集，旨在让任何用户都能独立验证其内容，无需信任数据发布者。数据集包含加密签名的收据、内核验证的定理列表和公式注册表。

• 许可证: Apache-2.0
• 规模: 少于 1000 条记录 (n<1K)
• 标签: provenance, attestation, dsse, sigstore, cosign, formal-verification, lean4, verify-it-yourself

数据集结构与配置

数据集包含三个主要配置，分别对应不同的数据类型：

配置名称	数据文件路径	描述
receipts	receipts/*.ndjson	加密签名的 DSSE 收据及验证数据
theorems	theorems/*.ndjson	Lean 4 内核验证的定理列表（逐字复制）
formulas	formulas/*.ndjson	公式注册表及其证明状态（逐字复制）

每个配置的 *.ndjson 文件均按日期分割（如 receipts/2026-06-12.ndjson），并且每个配置都包含一个 head.json 文件，记录链状态（计数、最后一个 ID、分片信息）。

每条记录都是一个桶信封 (bucket envelope)，格式如下：

json { "schema": "szl.hf.bucket.record/v1", "id": "<sha256>", "ts": "...", "source": "a11oy", "kind": "receipt|theorem|formula", "payload": { ... } }

记录 ID (id) 是基于 {source, kind, content} 的内容寻址，而非时间戳，这使得重新发布具有幂等性。

1. 收据 (receipts/)

收据包含两种签名方案，均为真实签名，不含未签名或占位信封：

签名方案 (payload.scheme)	含义	签名方式
ecdsa-p256-dsse-pae	a11oy Khipu 收据	使用 SZL Holdings 的 cosign 密钥，对 DSSE PAE 进行 ECDSA-P256-SHA256 签名
sigstore-keyless-dsse	治理门禁收据	在 CI 环境中使用 Sigstore 无密钥 方式（Fulcio 证书 + Rekor 透明度日志）签名

每个收据的 payload.envelope 包含完整的 DSSE 信封，payload.verify 提供验证方法。

验证 ecdsa-p256-dsse-pae 收据：

1. 重构 DSSE PAE (Pre-Authentication Encoding)：

   PAE = b"DSSEv1 " + len(payloadType) + b" " + payloadType + b" " + len(payload) + b" " + payload

   其中 payload 是 envelope.payload 经 Base64 解码后的内容。

2. 获取公钥：公钥发布在 https://raw.githubusercontent.com/szl-holdings/.github/main/cosign.pub。

3. 使用 ECDSA-P256 算法和 SHA256 哈希函数，对 PAE 进行签名验证。

4. 公钥内容（可用于验证）：

   -----BEGIN PUBLIC KEY----- MFkwEwYHKoZIzj0CAQYIKoZIzj0DAQcDQgAE/Jlv9FnwJ13l4QIZpr4IbTBUtVZ2 i+O7Jai/s7xsdXvOjmZGYhd36VxNQQahTSjWoYpPrSNhXbt/n7lsgi61xA== -----END PUBLIC KEY-----

验证 sigstore-keyless-dsse 收据：

1. 信封本身包含完整的 Sigstore 包（envelope._sigstore.bundle），包括 Fulcio 证书链和 Rekor 包含证明。
2. 使用 cosign 工具进行验证： bash cosign verify-blob-attestation --bundle bundle.json --new-bundle-format --certificate-identity-regexp github.com/szl-holdings/.* --certificate-oidc-issuer https://token.actions.githubusercontent.com statement.json

2. 定理 (theorems/)

该部分包含从 lutar-lean 的 VERIFIED_THEOREMS.md 文件中逐字复制的、经内核验证的定理列表。

• payload.markdown: 文件的逐字节内容。
• payload.content_sha256: 文件内容的 SHA256 哈希值，可用于交叉验证。
• payload.summary: 来源文件自身声明的计数和诚实性标记。
• payload.source_url: 定理来源的 URL。

这些定理由 Lean 内核检查，不包含任何 sorry。用户可以克隆 lutar-lean 仓库并自行运行构建进行验证。

3. 公式 (formulas/)

该部分包含 a11oy 标准注册表中的公式记录。每条记录包含：

• payload.name / payload.callable: 公式名称及其运行时函数。
• payload.proof_status: 从注册表的 PROOF_STATUS 中逐字复制的证明状态。

证明状态反映了 Lean 内核和 Doctrine v11 的诚实性表面，包括 PROVEN（已证明）、AXIOM（公理约束）、SORRY（未证明）、REAL（真实）和 CONJECTURE（猜想）。

诚实性与范围

该数据集遵循 a11oy 的 v11 诚实性原则：

• 定理 U 是 REAL but CONDITIONAL (在特定假设下证明），不是无条件证明。
• 猜想 1 (无条件的 Λ-唯一性) 是 OPEN 状态，且在 A1–A5 公理下经机器检查为假（存在显式反例）。
• 数据集不包含任何演示级别的 HMAC 收据或未加密签名的哈希链工件，只包含可通过公钥或透明度日志验证的材料。

来源

• 生产者: szl-holdings/a11oy 仓库的 szl_corpus_publish.py 脚本。
• 定理来源: szl-holdings/lutar-lean 仓库。
• 公钥: 发布在 szl-holdings/.github/cosign.pub 。
• 许可证: Apache-2.0。

搜集汇总

数据集介绍

构建方式

该数据集由a11oy系统的追加写入、内容寻址的客户端生成，并通过publish脚本发布至HuggingFace。数据采用目录结构组织，每个子目录下存有按日期分片的NDJSON文件和一个head.json记录链状态。记录以信封格式封装，包含schema、内容寻址的id、时间戳、来源、类型及载荷。每条记录都是幂等的，重复发布相同的逻辑记录会去重为单一存储条目，而真正的内容变更则以新记录形式追加，完整保留历史版本。

特点

数据集的核心特点在于其可验证性与诚实性。所有收据（receipt）都包含完整的密码学材料，支持离线签名验证，涵盖ECDSA-P256-DSSE和Sigstore无密钥两种真实签名方案，无需信任发布方。定理（theorem）和公式（formula）记录均从Lean4内核验证的源头逐字复制，内容哈希可与开源仓库交叉校验。数据集严格遵循诚实原则，不夸大任何声明，定理U明确标注为条件成立，猜想1标注为开放问题，每个证明状态都如实反映内核检查结果。

使用方法

开发者可直接通过HuggingFace数据集加载器读取各配置的NDJSON文件。对于ECDSA-P256-DSSE收据，可通过获取发布方公开公钥，重构DSSE PAE载荷并使用cryptography库验证ECDSA签名；对于Sigstore无密钥收据，则使用cosign工具并指定证书身份正则表达式进行验证。定理和公式记录可直接比较其content_sha256与上游GitHub仓库的实时内容，也可克隆lutar-lean仓库自行运行lake build来复现验证过程。数据集还支持通过a11oy控制台实时读取其承诺状态。

背景与挑战

背景概述

在形式化验证与可验证计算这一前沿交叉领域，确保数学定理的自动证明结果具备可独立复现的信任基础，构成了核心研究命题。a11oy Verifiable Corpus 数据集由 SZL Holdings 机构于2025年创建，旨在将签名凭证与证明表面（proof surface）以不可篡改、内容寻址的方式公开发布，使得任何第三方无需依赖机构本身的声誉即可完成离线验证。该数据集围绕 Lean 4 形式化验证引擎生成的定理列表、公式注册表及其证明状态记录，辅以基于 DSSE 签名的 ECDSA-P256 与 Sigstore keyless 双重签名体系，构建了一套完整的“自验证”证据链。其发布对于推动数学证明的可信传播、降低形式化验证的信任门槛具有显著学术与实践影响。

当前挑战

该数据集所解决的领域挑战集中体现在形式化证明结果的可验证性与信任传递问题上。传统上，定理证明结果依赖于发布机构的权威性，用户无法独立验证证明声明的正确性和完整性。该数据集通过加密签名与透明日志机制，使每条证明记录均可由任意验证者通过公开密钥或公钥基础设施完成离线核验，有效消除了对中心化信任的依赖。此外，构建过程中面临的核心挑战在于：如何在不引入营销性声明的前提下，忠实地映射 Lean 内核验证的证明状态，包括对有前提条件的证明（如 Theorem U）和开放性猜想（如 Conjecture 1）进行准确分类标注，同时维护追加日志的幂等性和不可伪造性。

常用场景

经典使用场景

在形式化验证与可审计基础设施的交汇领域，a11oy-verifiable-corpus 数据集为研究者提供了一种独特的可独立验证的凭证存储与发布范式。该数据集最经典的使用场景是作为可验证凭证的公开仓库，其中包含了由 ECDSA-P256 和 Sigstore 无密钥签名机制生成的 DSSE 收据，以及通过 Lean 4 定理证明器内核检查的定理列表。使用者无需信任数据集发布者，即可利用公开密钥或 Sigstore 透明度日志离线验证每一条记录的完整性与真实性，从而构建起一套无需信任第三方的可审计数据管道。这一场景尤其适用于需要公开证明数据完整性、来源可追溯且支持历史重放的学术与工程系统。

实际应用

在实际工程应用中，该数据集可作为构建去信任化审计系统的核心数据源。例如，区块链预言机、多方计算协议或软件供应链安全平台可将其作为公开可验证的凭证存储层，用于记录关键操作的数字签名与时间戳。开发者可以利用数据集中提供的标准 DSSE 收据格式与验证脚本，快速集成到 CI/CD 流水线中，实现代码签名、部署审批等环节的自主验证。此外，a11oy 控制台已演示了通过读取该数据集恢复已验证状态的功能，展示了 Hugging Face 作为主存储后端而非单向镜像的实用性，为构建公开透明的分布式审计基础设施提供了可复用的参考实现。

衍生相关工作

该数据集的发布驱动了一系列围绕可验证凭证与形式化证明的衍生工作。其中，作为数据源核心组件的 lutar-lean 项目提供了经过 Lean 内核检查的定理清单，其自动生成的 VERIFIED_THEOREMS.md 文件成为验证定理声明的权威参考。SzL Holdings 同时开发了用于生成与发布该数据集的 a11oy 客户端与 szl_hf_bucket 工具链，实现了追加写入与幂等发布特性。此外，Sigstore 无密钥签名方案在 CI 环境中的集成实践，以及 DSSE 信封格式在学术凭证领域的新应用，均因该数据集的公开而获得了更广泛的研究关注。这些工作共同构建了一个从定理形式化验证到可公开审计的完整技术栈。