Minimal trusted base
The trusted story starts at canonical certificate bytes and checker output, not at source generation or navigation metadata.
Nano Proof Auditor
Certificate-first proof verification for mathematical packages.
NPA draws a strict boundary between checked certificate evidence and helpful but untrusted metadata. This page introduces the toolchain, the trust model, and the package URLs under finitefield.org/npa/.
NPA tag
v0.1.1
Package toolchain pin from the npa-site catalog.
Rust
1.95.0
Toolchain version recorded by the source site.
Packages
2
npa-mathlib and npa-std are published under /npa/.
Theorems
750
Current theorem count surfaced from npa-mathlib.
Pinned toolchain
NPA_GIT_TAG = v0.1.1
RUST_TOOLCHAIN_VERSION = 1.95.0
Package audit trail
Package pages expose versions, licenses, module counts, theorem counts, and verification commands in one stable URL family.
Mathematics publishing
As more npa-mathlib theorem introductions are published, theorem pages can live under the recommended mathematics URL structure.
Trust boundary
Checked evidence and sidecars are intentionally separated.
NPA-compatible repositories can include source files, replay data, theorem indexes, and reports. The trusted boundary is the checked certificate path; the rest supports discovery, review, and navigation.
Certificates and checker results
The verifier output and .npcert files are the artifacts treated as mathematical checking evidence.
Metadata and replay data
meta.json, replay.json, indexes, and generated navigation files help readers inspect proofs, but they are not the checker boundary.
Package URLs
Use short, brand-owned package paths under /npa/.
The URL strategy treats NPA as a research brand and long-term company asset, so package pages stay under finitefield.org/npa/ rather than the generic OSS section.
npa-mathlib
Formalized mathematics library
The public theorem-library package currently exposing 61 modules and 750 theorem entries from the npa-site catalog.
0.1.27
Version
61
Modules
750
Theorems
npa-std
Standard logic and arithmetic
The standard package path is reserved at /npa/std/ for logic and arithmetic primitives used by NPA-compatible packages.
0.1.0
Version
2
Modules
MIT
License
Local audit
Keep verification commands visible next to the package story.
The source site presents NPA as a local auditing workflow. These commands preserve that operational framing in the company site.
Audit certificates
npa package verify-certs --root ../npa-mathlib --checker reference --jsonCheck package policy
npa package check --root ../npa-mathlib --json