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 确认。