NPA / 证书优先的证明检查

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

本页把 Math Lab 中的 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、WASM 或真实证明证书。它可视化真实产物必须满足的不依赖源文件的检查顺序。

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 三个公开仓库都通过 LICENSE 元数据显示 Apache-2.0 许可。	已核验的公开主张	S01 / S02 / 2026-07-02	大版本发布时复核 LICENSE。

仓库与许可

明确代码、包仓库和组织可见性。

仓库链接是公开源码指针，不保证本页始终与 GitHub 最新状态同步。

4 个仓库

finitefield-org

npa

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

许可: 2026-07-02 已从 LICENSE 确认 Apache-2.0。
验证: 最新 Git 标签：v0.2.0。GitHub 的 releases/latest 页面未发布。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 仓库是公开代码状态的来源。许可、当前标签、公开可见性和发布表述已作为 M10-T14 最终回读于 2026-07-02 复核。

证明生态防护线

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

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

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