指南与信任策略

学习如何在本地验证数学证明，并理解我们的密码学信任模型。

1. 本地验证（审计）

独立审计是 Nano Proof Auditor 的核心价值。按照以下步骤，可在自己的机器上用密码学方式验证任意证明。

确认系统已安装 Rust toolchain 与 Cargo。
从源码或包管理器安装 NPA CLI 工具：
```
cargo install npa-cli
```
进入任意 package index 目录，例如 npa-mathlib，并在本地运行验证命令：
```
npa package verify-certs --root ../npa-mathlib --checker reference --json
```

NPA 对数学常量和公理进行分类，用于审计逻辑可靠性。

确定性 hash、验证器日志和 checker 签名（.npcert）属于可信证据。源代码文本、proof replay 步骤和文档 overlay 是非可信 sidecar，只用于展示。

为避免逻辑矛盾，例如推出 False，定理会按严格公理策略审计。Lean 的标准经典公理（Quot.sound、Propext、Classical.choice）在白名单内。未验证公理或自定义假设会触发策略违规。

快速了解本 registry 使用的形式化验证概念。

由密码学证书（.npcert）验证的数学陈述，证书表明 sound proof term 已被检查。

无需证明而被假设的陈述。公理是逻辑基础，但未经检查的自定义公理可能引入矛盾。

由构造子定义的数据类型，例如由 zero 和 successor 定义的自然数。

在 Curry-Howard 同构下表示定理证明的数学表达式。

逐步重建 proof term，并在 kernel 内验证其有效性的过程。