公开状态
研究与实现仓库
GitHub 仓库是公开的，但本页描述的是研究与实现仓库，不是已部署服务。
返回 Math Lab
NPA / Certificate-first proof checking
NPA：先暴露证明证据边界，再信任结果。
本页把 Math Lab 中的 NPA 部分重构为独立的 evidence page：公开状态、trust model、proof pipeline、claim register、repositories、sources，以及明确的非替代表述。
- 公开状态
- 研究与实现仓库
- 作为研究与实现展示，不作为生产保障服务。
- 公开信息复核
- 2026-07-02 / NPA v0.2.0
- 已确认最新 git tag：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 tag 为 v0.2.0，npa-std 为 v0.1.0，npa-mathlib 为 v0.1.30。包 README 的 pin 作为仓库自身语境展示，不合并成一个 NPA 总版本主张。
Public status
说明什么是公开状态、什么是证据，以及复核日期。
本页公开自身依据：本地 truth snapshot、公开仓库 source，以及发布前最终复核日期。
公开信息复核
2026-07-02
公开信息 readback 已于 2026-07-02 完成。原始素材重建仍以 2026-06-21 本地 truth snapshot 为基准。
Evidence
Certificates and hashes
来源快照记录 canonical .npcert、certificate_hash、export_hash、axiom_report_hash 和 checker verdict。
License
Apache-2.0 已确认
2026-07-02 已通过公开 LICENSE metadata 确认 npa、npa-std、npa-mathlib 均为 Apache-2.0。
Boundary
NPA 不是 Lean 或 Rocq 的实用替代品。浏览器模拟不会运行 NPA 本体。public tags、license 和 repository visibility 已作为最终发布 readback 于 2026-07-02 复核。
Trust boundary
只让 canonical certificate 穿过 evidence boundary。
边界问题不是哪个 tool 看起来更复杂，而是哪一个 artifact 在 independent checking 后可以成为证据。
Parser、elaborator、tactics、automation、theorem search、plugins、AI systems、source files、replay files、theorem indexes、publish plans、CI status、release pages 和 registry metadata 都留在 untrusted candidate side。
Proof pipeline / 说明用模拟
展示从 certificate bytes 到 checking evidence 的完整 pipeline。
浏览器模拟不会运行 NPA 本体、Rust、WASM 或真实 proof certificate。它可视化真实 artifact 必须满足的 source-free checking 顺序。
CLI evidence path
npa package verify-certs --root . --checker reference --json
NPA / audit trace
READY
- 01 Certificate formatcanonical .npcert bytes / parseable certificate / format check WAIT
- 02 Certificate hashcertificate bytes / certificate_hash / deterministic digest WAIT
- 03 Kernel verdictcertificate / accept or reject / Rust verifier report WAIT
- 04 Reference checkerhash-pinned certificate / independent accept or reject / source-free checker report WAIT
- 05 Axiom reportchecked package / axiom_report_hash / assumption inventory WAIT
Verdict
说明用 pipeline 尚未运行。运行说明后，将按顺序标记 source-free checking path。
Claim register
区分证据、时间敏感事实和边界主张。
本页不依赖松散的研究介绍。每个公开表述都对应本地 truth snapshot、来源和发布前动作。
| 主张 | 公开表述 | 状态 | 来源 | 发布前动作 |
|---|---|---|---|---|
| CL-001 | NPA 是 certificate-first。可审计边界是 canonical .npcert artifact 及其周围的检查路径。 | 已核验的公开主张 | S01 / 2026-07-02 | README 变化时复核。 |
| CL-002 | 2026-07-02 的公开信息复核显示，NPA 仓库的最新 git tag 是 v0.2.0。相关包 README 仍保留各仓库自己的 pin，因此版本表述按仓库分别限定。 | 公开信息已复核 | S01 / S02 / 2026-07-02 | 版本 tag 表述按仓库分别限定。 |
| CL-003 | 本地 truth snapshot 记录 Rust 1.95.0 toolchain pin；它不作为宣传主张展示。 | 已核验，时间敏感 | S01 / 2026-07-02 | 只有展示 toolchain 版本时才复核。 |
| CL-004 | NPA 不是 Lean 或 Rocq 的实用替代品。任何比较旁边都必须保留这个边界。 | 已核验的边界主张 | S01 / S03 / S05 / 2026-07-02 | 保留免责声明。 |
| CL-005 | npa-std 和 npa-mathlib 是 finitefield-org 下公开的两个独立 theorem package 仓库。 | 已核验的公开主张 | S01 / S02 / 2026-07-02 | 发布延迟或仓库变化时再次复核可见性。 |
| CL-006 | npa、npa-std、npa-mathlib 三个公开仓库都通过 LICENSE metadata 显示 Apache-2.0 许可。 | 已核验的公开主张 | S01 / S02 / 2026-07-02 | 大版本发布时复核 LICENSE。 |
Repositories and license
明确代码、package repository 和 organization visibility。
Repository link 是公开 source 指针，不保证本页始终与 GitHub 最新状态同步。
4 个仓库
finitefield-org
npa
certificate-first proof assistance 与 verification toolchain。
- License
- 2026-07-02 已从 LICENSE 确认 Apache-2.0。
- Verification
- 最新 git tag：v0.2.0。GitHub releases/latest 未发布。README 当前 toolchain reference：NPA_GIT_TAG=v0.2.0。
experimentalRust / OCamlcertificate-first
打开仓库
finitefield-org
npa-std
NPA proof source 的 standard theorem package repository。
- License
- 2026-07-02 已从 LICENSE 确认 Apache-2.0。
- Verification
- 最新 git tag 和 GitHub release：v0.1.0。README package metadata version：0.1.0；package toolchain pin：NPA_GIT_TAG=v0.1.1。
experimentaltheorem packageproof source
打开仓库
finitefield-org
npa-mathlib
formal mathematics library 研究仓库。
- License
- 2026-07-02 已从 LICENSE 确认 Apache-2.0。
- Verification
- 最新 git tag：v0.1.30。最新 GitHub release：v0.1.9。README package metadata version：0.2.1；package toolchain pin：NPA_GIT_TAG=v0.1.1。
researchformal mathematicslibrary
打开仓库
finitefield-org
Finite Field GitHub organization
Lab repository family 的公开组织快照。
- License
- 适用各仓库自己的 license
- Verification
- 2026-07-02 的 GitHub API readback 显示 npa、npa-std、npa-mathlib 均为公开仓库。
public indexvisibility snapshotsource
打开组织
没有仓库符合当前搜索条件。
GitHub 仓库是公开代码状态的 source。license、current tags、public visibility 和 release wording 已作为 M10-T14 最终 readback 于 2026-07-02 复核。
Proof ecosystem guard
比较 proof tool 前，先明确角色。
这是一张角色表，不是排名。Lean 和 Rocq 仍是参考性的 proof assistant ecosystem；NPA 在这里作为 certificate-centered 的研究与实现工作呈现。
| 项目 | Lean | Rocq | NPA |
|---|---|---|---|
| 定位 | 开源 programming language 与 proof assistant。 | 具有长期研究历史的 interactive theorem prover。 | 面向 certificate-first checking 的研究与实现仓库。 |
| 典型用途 | 数学、软件验证和编程。 | 数学、规格、程序验证和 extraction。 | 研究 proof certificate、独立检查和小 trusted base。 |
| 证据边界 | Lean 自身的 trusted kernel 和生态定义检查边界。 | Rocq 自身的 kernel 和已检查 development 定义检查边界。 | canonical .npcert 从 generation 进入 checking，形成边界。 |
| 本页处理方式 | 学习、比较和互操作的参考。 | 学习、比较和 formalization 方法的参考。 | Finite Field 的研究项目，不是产品承诺。 |
| 边界 | 仍然需要专业知识。 | 仍然需要专业知识。 | 目前，NPA 不是 Lean 或 Rocq 的实用替代品。 |
Sources
把 source map 放在解释旁边发布。
展示 source map，让读者能区分哪些主张来自公开仓库、proof tool 官方网站和公司上下文。
S01
finitefield-org/npa
NPA purpose、trust model、当前仓库 tag v0.2.0、commands、repository layout 和 license 的 primary source。
打开来源 S02Finite Field GitHub organization
2026-07-02 复核 public repository visibility、latest git tags、release pages 和 Lab repository family snapshot 的 primary source。
打开来源 S03Lean official site
Lean 公开定位的 primary source。2026-07-02 已确认。
打开来源 S04Lean language reference
dependent type theory 和 kernel reference context 的 primary source。2026-07-02 已确认。
打开来源 S05Rocq Prover official site
Rocq 公开定位的 primary source。2026-07-02 已确认。
打开来源 S06FINITE FIELD company site
Finite Field brand 和 business context 的 company source。
打开来源01 本页是产品保证吗？
不是。这里把 NPA 作为研究与实现仓库展示。
02 NPA 能替代 Lean 或 Rocq 吗？
不是。NPA 不是 Lean 或 Rocq 的实用替代品。
03 本页会执行真实的 NPA verification 吗？
不能。浏览器模拟不会运行 NPA 本体、Rust、WASM 或真实 proof certificate。
04 这里什么算证据？
certificate artifact、deterministic hash、Rust kernel/verifier result、source-free reference checker result 和 axiom report 构成 checking side 的证据。
05 哪些事实需要复核？
当前公开版本、仓库可见性、toolchain pin、许可文本和来源表述已于 2026-07-02 复核。