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 憑證雜湊憑證位元組 / certificate_hash / 確定性摘要等待
03 核心判定憑證 / 接受或拒絕 / Rust 驗證器報告等待
04 參考檢查器由雜湊固定的憑證 / 獨立接受或拒絕 / 不依賴原始碼的檢查器報告等待
05 公理報告已檢查的套件 / axiom_report_hash / 假設清單等待

判定

說明用流程尚未執行。

執行說明後，將按順序標記不依賴原始碼的檢查路徑。

主張登記表

區分證據、時間敏感事實與邊界主張。

本頁不依賴鬆散的研究介紹。每個公開表述都對應本地事實快照、來源與釋出前動作。

主張	公開表述	狀態	來源	釋出前動作
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 Release。README 目前的工具鏈參照：NPA_GIT_TAG=v0.2.0。

實驗Rust / OCaml憑證優先

開啟倉庫

finitefield-org

npa-std

NPA 證明原始碼的標準定理套件倉庫。

授權: 已於 2026-07-02 從 LICENSE 確認 Apache-2.0。
驗證: 最新 Git 標籤與 GitHub Release：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 Release：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 的 M10-T14 最終讀回中複核。

證明生態防護線

比較證明工具前，先明確角色。

這是一張角色表，不是排名。Lean 與 Rocq 仍是參考性的證明輔助系統生態；NPA 在這裡作為以憑證為中心的研究與實作工作呈現。

項目	Lean	Rocq	NPA
定位	開源程式語言與證明輔助系統。	具有長期研究歷史的互動式定理證明器。	面向憑證優先檢查的研究與實作倉庫。
典型用途	數學、軟體驗證與程式設計。	數學、規格、程式驗證與程式碼提取。	研究證明憑證、獨立檢查與小型可信基礎。
證據邊界	Lean 自身的可信核心與生態定義檢查邊界。	Rocq 自身的核心與已檢查開發成果定義檢查邊界。	標準化 .npcert 從產生側進入檢查側，形成邊界。
本頁處理方式	學習、比較與互操作的參考。	學習、比較與形式化方法的參考。	Finite Field 的研究專案，不是產品保證。
邊界	仍然需要專業知識。	仍然需要專業知識。	目前，NPA 不是 Lean 或 Rocq 的實務替代品。