01 / 邊界
保持可信基礎小而清晰
不要把複雜產生器或 AI 放在信任中心。應明確呈現較小的檢查側。
Lab 原則
不只發布結果，也發布檢查邊界。
“能執行”“速度快”或“已證明”這樣的結論本身不夠。我們會把輸入、假設、可信部分、可獨立檢查的產物與未解決問題分開呈現。
02 / 證據
讓證據成為產物
把憑證、雜湊、假設列表、基準條件與日誌留下來，方便他人檢查。
03 / 重現
為可重現性設計
固定工具鏈、輸入資料、執行命令與評價標準，使結果能夠再次檢查。
04 / 如實說明
不過度表述研究狀態
把實用方法、實驗與研究分開呈現。限制條件應放在結果旁邊。
方法複核
這是在說明可用於客戶專案之前，仍需確認範圍、責任、適用證據與核准的方法類別。
實驗
已有可執行實作，但規模、相容性、效能或規格仍可能變化。必須附帶版本與重現步驟。
研究
設計、評價、證明或實作仍在進行中。這不意味著商業可用或已經完成。
研究組合
按成熟度與產物查看研究。
每張卡片都顯示成熟度、產物、目前狀態與下一步驗證。搜尋與篩選只使用瀏覽器端狀態。
8 項
實驗
開源
01
Nano Proof Auditor
憑證優先的證明工具鏈
一個研究工具鏈，把標準化證明憑證與小型檢查基礎放在依賴證明複核的中心。
- 產物
- 原始碼 / 規格 / CI 範本
- 目前
- v0.1.1 公開快照
- 下一步驗證
- 外部定理包與獨立檢查
實驗
開源
02
NPA Standard Library
Logic / Nat / List / Algebra
用於重複使用 NPA 基礎內容的標準定理包倉庫。
- 產物
- 原始碼 / 證明包
- 目前
- 已拆分的公開倉庫
- 下一步驗證
- 套件範圍與相容性
研究
開源
03
NPA Math Library
形式化數學庫
將數學定理作為可獨立檢查的證明包保存的函式庫方向。
- 產物
- 原始碼 / 證明包
- 目前
- 正在開發的公開倉庫
- 下一步驗證
- 函式庫結構與依賴稽核
方法複核
方法
04
約束規劃模型
排程 / 路線 / 分配
在排班、拜訪、路線、生產與分配工作中，分離硬約束與評價指標的方法。
- 產物
- 模型 / 原型 / 說明報告
- 目前
- 按方法複核呈現，不主張部署成果。
- 下一步驗證
- 客戶證據與範圍核准
研究
測量
05
可重現的求解器評價
基準與證據
在提出效能主張前，先固定實例集、硬體、時間限制、隨機種子與原始日誌的計畫。
- 產物
- 基準登記 / 原始日誌 / 報告
- 目前
- 研究計畫設計
- 下一步驗證
- 首個公開基準語料
研究
形式化方法
06
關鍵業務邏輯驗證
業務系統的不變量
研究如何把費用、權限、庫存與狀態遷移分離為規格與不變量。
- 產物
- 規格 / 不變量 / 測試或證明報告
- 目前
- 範圍研究
- 下一步驗證
- 選擇一個邊界明確、接近生產情境的案例
實驗
工程
07
Rust 中的小型可信元件
小型可信元件
把檢查器與雜湊等信任關鍵元件控制在可檢查範圍內的實作工作。
- 產物
- NPA 核心 / 憑證包 / 參考檢查器
- 目前
- NPA 中的公開實作
- 下一步驗證
- 獨立檢查器相容性
研究
AI × 證明
08
AI 輔助與獨立檢查
自由產生，嚴格驗證
一種研究方向：AI 位於候選產生側，最終證據必須被獨立檢查。
- 產物
- 候選產生器 / 憑證 / 檢查器報告
- 目前
- 符合 NPA 信任模型的研究方向
- 下一步驗證
- 實測編寫流程
沒有符合條件的研究領域。
請換一個關鍵詞，或把成熟度篩選改回全部。
Nano Proof Auditor
把證明產生與真正信任的對象分開。
NPA 是面向依賴證明的憑證優先證明工具鏈。前端、證明策略、定理搜尋、外掛、AI、原始檔與 CI 狀態都可以幫助產生候選，但它們不是可信證明證據。
實驗開源APACHE-2.0
目前快照
v0.1.1
公開資訊於 2026-06-21 確認。
主要核心
Rust
Rust 驗證器與核心屬於檢查側。
稽核產物
.npcert
標準化憑證位元組是需要檢查的對象。
複核點
人工複核
發布前必須複核倉庫狀態與套件可見性。
信任邊界瀏覽器
逐項查看哪些內容被信任，哪些內容不被信任。
點擊每個節點，查看它的作用、產出以及仍需進行的檢查。
不可信
已檢查
重要邊界
NPA 目前不是 Lean 或 Rocq 的實務替代品。本頁說明以憑證為中心的研究設計，並不保證商業系統沒有缺陷，也不保證自動定理求解。
憑證檢查 / 說明用模擬
體驗憑證被檢查的流程。
瀏覽器中的互動只用來說明檢查流程，不會執行 NPA、Rust、WASM 或真實的證明憑證。
CLI 範例
npa package verify-certs --root . --checker reference --json
NPA / 稽核軌跡
待執行
- 01 讀取憑證標準化位元組 / 格式 等待
- 02 檢查憑證雜湊憑證雜湊 等待
- 03 透過核心檢查依賴證明檢查 等待
- 04 用參考檢查器複核不依賴原始碼的判定 等待
- 05 比對公理報告公理報告雜湊 等待
判定
說明尚未執行。執行說明後，會依序顯示各個步驟。
證明生態
明確角色，而不是替工具排名。
Lean 與 Rocq 是成熟的證明輔助系統。這裡呈現的 NPA 是以憑證為中心的研究與實作專案，並不是替代品排名。
| 項目 | Lean | Rocq | NPA |
|---|---|---|---|
| 定位 | 開源程式語言與證明輔助系統。 | 擁有長期研究歷史的互動式定理證明器。 | 用於研究憑證優先檢查的實作倉庫。 |
| 典型用途 | 數學、軟體驗證與程式設計。 | 數學、規格、程式驗證與程式碼抽取。 | 研究證明憑證與獨立檢查。 |
| 重點 | 可擴充性、函式庫與互動式證明。 | 表達能力、成熟方法與函式庫。 | 小型可信基礎與標準化憑證。 |
| 本頁中的定位 | 學習、比較與互操作的參照。 | 學習、比較與形式化方法的參照。 | Finite Field 的研究專案。 |
| 邊界 | 仍需要專業知識。 | 仍需要專業知識。 | 目前不作為 Lean 或 Rocq 的實務替代品。 |
研究方法
把「成功了」變成可重複的檢查流程。
當別人能夠在相同條件下重新執行、檢查並拒絕結果時，結果才更可靠。
問題
定義需要檢查的內容：效能、正確性、相容性或範圍。
假設
在評價前寫明假設、排除項、公理、資料缺口與偏差。
產物
保留原始碼、憑證、輸入、執行日誌與雜湊。
獨立檢查
透過不同於產生側的路徑檢查結果。
基準
固定硬體、版本、時間限制、實例集與隨機種子。
邊界
公開失敗、未支援案例、效能邊界與下一步驗證。
可重現性檢查表
檢查研究發布還缺哪些內容。
這份清單只在瀏覽器中處理。它不是認證分數。
準備度
0%下一步
先定義研究問題與成功條件。在決定產物格式前，先固定需要比較或檢查的內容。
公開產物
從一個入口追蹤公開產物。
本頁不在執行期間呼叫 GitHub API。倉庫狀態是已複核的快照，發布前必須再次確認。
4 個公開產物
finitefield-org
npa
憑證優先的證明工具鏈
驗證
package verify-certs
finitefield-org
npa-std
標準定理包
角色
Std.Logic / Nat / List
finitefield-org
npa-mathlib
形式化數學庫
角色
形式化定理包
GitHub
finitefield-org
公開倉庫索引
索引
全部公開倉庫
沒有符合條件的公開產物。
發布方針
公開倉庫、研究筆記與基準應包含檢查日期、成熟度、重現步驟與已知限制。星數與提交數不作為研究品質指標呈現。
從 Lab 到業務現場
把研究紀律帶入業務系統設計。
並不是每個客戶的業務系統都需要定理證明。真正有用的遷移，是明確哪些部分必須被信任、比較、檢查、修正，並由人最終核准。
Lab 方法
把產生、計算與最終檢查分開，而不是同等信任每一層。
把輸入、輸出、憑證、雜湊與日誌保留下來，作為可複核的產物。
在比較結果之前，先固定資料、版本、命令與評價條件。
約束、失敗案例與未解事項，應與結果一樣清楚公開。
客戶系統
定義誰輸入、誰複核、誰進行人工調整、誰確認結果。
顯示約束、評價分數、被拒絕的候選與未解事項。
保留條件變更、計算執行與最終核准記錄。
讓自動輸出可以被操作人員修正、拒絕與說明。
01 Math Lab 是合約開發服務嗎？
不是。這裡用於發布研究態度與產物。在客戶討論中，我們會區分可應用的方法、還需要驗證的方法，以及仍處於研究階段的主題。
02 NPA 能替代 Lean 或 Rocq 嗎？
不能。目前 NPA 不是 Lean 或 Rocq 的實務替代品。它是圍繞憑證、獨立檢查與小型可信基礎的研究與實作專案。
03 你們會直接信任 AI 產生的證明嗎？
不能直接信任。AI、搜尋與證明策略可以幫助產生候選。我們關注的是最終憑證是否能被獨立於產生路徑的檢查器接受。
04 形式化驗證能消除所有缺陷嗎？
不會。形式化方法會針對明確規格檢查特定性質。錯誤的規格、範圍外程式碼、執行操作與外部服務仍需要單獨審查。
05 這與業務系統開發有關嗎？
相關。我們通常逐步應用這種紀律：約束、結果原因、計算歷史、權限邊界，以及重要業務邏輯的檢查。
來源快照 / 2026-06-21
NPA 相關主張基於 finitefield-org/npa 倉庫快照。Lean 與 Rocq 的定位基於其官方網站。倉庫狀態、最新標籤與方法複核表述已於 2026-06-28 確認。