NPA / 证书优先的证明检查

NPA：先暴露证明证据边界，再信任结果。

本页集中整理 Math Lab 中与 NPA 有关的内容，说明哪些内容已公开、如何建立可信性、如何检查证明、哪些主张有证据支持、源代码仓库位于何处，以及为什么 NPA 不能替代现有证明助手。

公开状态: 研究与实现仓库; 作为研究与实现展示，不作为生产保障服务。
公开信息复核: 2026-07-02 / NPA v0.2.0; 已确认最新 Git 标签：npa v0.2.0、npa-std v0.1.0、npa-mathlib v0.1.30。
许可: Apache-2.0; 2026-07-02 已确认 npa、npa-std、npa-mathlib 均为 Apache-2.0。

公开信息复核：2026-07-02。NPA 仓库最新 Git 标签为 v0.2.0，npa-std 为 v0.1.0，npa-mathlib 为 v0.1.30。各仓库 README 中的固定版本仅按各自上下文说明，不合并为统一的 NPA 版本。

展示证书检查和信任边界确认的 NPA 证据页预览 — 该视觉是证书检查结果和信任边界说明的静态预览，不是实时 NPA 轨迹。

公开状态

说明哪些内容已公开、哪些可作为证据，以及各自的最后复核时间。

本页公开自身依据：本地事实快照、公开仓库来源，以及发布前最终复核日期。

公开状态

研究与实现仓库

GitHub 仓库是公开的，但本页描述的是研究与实现仓库，不是已部署服务。

公开信息复核

2026-07-02

公开信息已于 2026-07-02 完成复核；必要之处也会引用经过核对的 2026-06-21 本地快照。

证据

证书和哈希

来源快照记录规范化 .npcert、证书哈希、导出哈希、公理报告哈希和检查器判定。

许可

Apache-2.0 已确认

已于 2026-07-02 通过公开 LICENSE 文件确认 npa、npa-std、npa-mathlib 均采用 Apache-2.0 许可。

边界

NPA 不是 Lean 或 Rocq 的实用替代品。浏览器模拟不会运行 NPA 本体。公开标签、许可和仓库可见性已作为最终发布回读于 2026-07-02 复核。

信任边界

只允许规范化证书跨越证据边界。

边界的判断不在于工具看起来多么复杂，而在于哪些产物经独立检查后可以被视为证据。

解析器、展开器、证明策略、自动化、定理搜索、插件、AI 系统、源文件、重放文件、定理索引、发布计划、CI 状态、发布页面和登记元数据，都留在不可信候选侧。

证明流程 / 演示

完整展示证书字节如何成为可独立检查的证据。

浏览器模拟不会运行 NPA、Rust、WebAssembly 或实际证明证书，只用于展示真实产物必须通过的不依赖源文件的检查顺序。

CLI 证据路径

npa package verify-certs --root . --checker reference --json

NPA / 审计轨迹 待运行

01 证书格式规范化 .npcert 字节 / 可解析的证书 / 格式检查等待
02 证书哈希证书字节 / 证书哈希 / 确定性摘要等待
03 内核判定证书 / 接受或拒绝 / Rust 验证器报告等待
04 参考检查器带哈希的证书 / 独立的接受或拒绝 / 不依赖源文件的检查器报告等待
05 公理报告已检查的包 / 公理报告哈希 / 假设清单等待

判定

演示流程尚未运行。

运行说明后，将按顺序标记不依赖源文件的检查路径。

主张登记表

区分证据、具有时效性的事实和适用范围声明。

本页不采用含糊的研究宣传，而是把每项公开主张与本地事实快照、信息来源和发布前必须完成的操作对应起来。

主张	公开表述	状态	来源	发布前动作
CL-001	NPA 采用证书优先的设计。可审计边界是规范化的 .npcert 产物，以及围绕它的检查路径。	已核验的公开主张	S01 / 2026-07-02	README 变化时复核。
CL-002	2026-07-02 的公开信息复核显示，NPA 仓库的最新 Git 标签是 v0.2.0。相关包 README 仍保留各仓库自己的固定版本，因此版本表述按仓库分别限定。	公开信息已复核	S01 / S02 / 2026-07-02	版本标签表述按仓库分别限定。
CL-003	本地事实快照记录 Rust 1.95.0 工具链固定版本；它不作为宣传主张展示。	已核验，时间敏感	S01 / 2026-07-02	只有展示工具链版本时才复核。
CL-004	NPA 不是 Lean 或 Rocq 的实用替代品。任何比较旁边都必须保留这个边界。	已核验的边界主张	S01 / S03 / S05 / 2026-07-02	保留免责声明。
CL-005	npa-std 和 npa-mathlib 是 finitefield-org 下公开的两个独立定理包仓库。	已核验的公开主张	S01 / S02 / 2026-07-02	发布延迟或仓库变化时再次复核可见性。
CL-006	npa、npa-std、npa-mathlib 三个公开仓库均发布了 Apache-2.0 LICENSE 文件。	已核验的公开主张	S01 / S02 / 2026-07-02	大版本发布时复核 LICENSE。

仓库与许可

清晰展示代码仓库、软件包仓库及其发布组织。

仓库链接仅用于指向公开来源，并不保证本页与 GitHub 的最新状态一致。

4 个仓库

finitefield-org

npa

证书优先的证明辅助与验证工具链。

许可: 2026-07-02 已从 LICENSE 确认 Apache-2.0。
验证: 最新 Git 标签：v0.2.0。尚未发布 v0.2.0 的 GitHub Release。README 当前工具链引用：NPA_GIT_TAG=v0.2.0。

实验Rust / OCaml证书优先

打开仓库

finitefield-org

npa-std

面向 NPA 证明源码的标准定理包仓库。

许可: 2026-07-02 已从 LICENSE 确认 Apache-2.0。
验证: 最新 Git 标签和 GitHub 发布：v0.1.0。README 包元数据版本：0.1.0；包工具链固定版本：NPA_GIT_TAG=v0.1.1。

实验定理包证明源码

打开仓库

finitefield-org

npa-mathlib

形式化数学库研究仓库。

许可: 2026-07-02 已从 LICENSE 确认 Apache-2.0。
验证: 最新 Git 标签：v0.1.30。最新 GitHub 发布：v0.1.9。README 包元数据版本：0.2.1；包工具链固定版本：NPA_GIT_TAG=v0.1.1。

研究形式化数学库

打开仓库

finitefield-org

Finite Field GitHub 组织

Lab 仓库系列的公开组织快照。

许可: 适用各仓库自己的许可
验证: 2026-07-02 的 GitHub API 回读显示 npa、npa-std、npa-mathlib 均为公开仓库。

公开索引可见性快照来源

打开组织

GitHub 仓库是公开代码状态的来源。相关许可、标签、仓库可见性和发布说明已于 2026-07-02 完成最终复核。

证明工具比较边界

比较证明工具前，先明确角色。

这是一张角色表，不是排名。Lean 和 Rocq 仍是参考性的证明辅助系统生态；NPA 在这里作为以证书为中心的研究与实现工作呈现。

项目	Lean	Rocq	NPA
定位	开源编程语言与证明辅助系统。	具有长期研究历史的交互式定理证明器。	面向证书优先检查的研究与实现仓库。
典型用途	数学、软件验证和编程。	数学、规格、程序验证和代码提取。	研究证明证书、独立检查和小型可信基础。
证据边界	Lean 自身的可信内核和生态定义检查边界。	Rocq 自身的内核和已检查开发成果定义检查边界。	规范化 .npcert 从生成侧进入检查侧，形成边界。
本页处理方式	学习、比较和互操作的参考。	学习、比较和形式化方法的参考。	Finite Field 的研究项目，不是产品承诺。
边界	仍然需要专业知识。	仍然需要专业知识。	目前，NPA 不是 Lean 或 Rocq 的实用替代品。