Public status
Research and implementation repository
The GitHub repository is public, but this page describes a research and implementation repository, not a deployed service.
Back to Math Lab
NPA / Certificate-first proof checking
NPA: expose the proof evidence boundary before trusting a result.
This page reconstructs the NPA section from Math Lab as an independent evidence page: public status, trust model, proof pipeline, claim register, repositories, sources, and explicit non-replacement language.
- Public status
- Research repository
- Shown as research and implementation, not as a production assurance service.
- Public recheck
- 2026-07-02 / NPA v0.2.0
- Latest git tags checked: npa v0.2.0, npa-std v0.1.0, npa-mathlib v0.1.30.
- License
- Apache-2.0
- Apache-2.0 was verified for npa, npa-std, and npa-mathlib on 2026-07-02.
Public recheck: 2026-07-02. The NPA repository latest git tag is v0.2.0; npa-std is v0.1.0; npa-mathlib is v0.1.30. Package README pins are shown as repository-specific context and are not flattened into one NPA version claim.
Public status
State what is public, what is evidence, and when it was rechecked.
This page makes the page's basis visible: a local truth snapshot, a public repository source, and the final prelaunch readback date.
Public recheck
2026-07-02
The public-source readback was completed on 2026-07-02. The original source reconstruction still uses the 2026-06-21 local truth snapshot.
Evidence
Certificates and hashes
The source snapshot records canonical .npcert, certificate_hash, export_hash, axiom_report_hash, and checker verdicts.
License
Apache-2.0 verified
Apache-2.0 was verified for npa, npa-std, and npa-mathlib through public LICENSE metadata on 2026-07-02.
Boundary
NPA is not a practical replacement for Lean or Rocq. The distributed browser inspection simulation does not run NPA itself. Public tags, license, and repository visibility were checked on 2026-07-02 for the final publication readback.
Trust boundary
Move only a canonical certificate across the evidence boundary.
The boundary is not about which tool looks sophisticated. It is about which artifact is allowed to become evidence after independent checking.
Parser, elaborator, tactics, automation, theorem search, plugins, AI systems, source files, replay files, theorem indexes, publish plans, CI status, release pages, and registry metadata stay on the untrusted candidate side.
Proof pipeline / explanatory simulation
Show the exact pipeline from certificate bytes to checking evidence.
The browser simulation does not run NPA itself, Rust, WASM, or real proof certificates. It visualizes the source-free checking order that real artifacts must satisfy.
CLI evidence path
npa package verify-certs --root . --checker reference --json
NPA / audit trace
READY
- 01 Certificate formatcanonical .npcert bytes / parseable certificate / format check WAIT
- 02 Certificate hashcertificate bytes / certificate_hash / deterministic digest WAIT
- 03 Kernel verdictcertificate / accept or reject / Rust verifier report WAIT
- 04 Reference checkerhash-pinned certificate / independent accept or reject / source-free checker report WAIT
- 05 Axiom reportchecked package / axiom_report_hash / assumption inventory WAIT
Verdict
The explanatory pipeline has not run yet.Run the explanation to mark the source-free checking path in order.
Claim register
Separate evidence, time-sensitive facts, and boundary claims.
The page does not depend on loose research copy. Each public statement is tied to a local truth snapshot, a source, and a publication action.
| Claim | Public wording | Status | Source | Publication action |
|---|---|---|---|---|
| CL-001 | NPA is certificate-first: the auditable boundary is the canonical .npcert artifact and the checking path around it. | Verified public claim | S01 / 2026-07-02 | Review when the README changes. |
| CL-002 | The 2026-07-02 public recheck found the NPA repository latest git tag at v0.2.0. Related package READMEs still show repository-specific pins, so version wording stays scoped by repository. | Verified public recheck | S01 / S02 / 2026-07-02 | Keep tag wording scoped by repository. |
| CL-003 | The local truth snapshot records a Rust 1.95.0 toolchain pin; it is not used as a marketing claim. | Verified, time-sensitive | S01 / 2026-07-02 | Recheck if the toolchain version is displayed. |
| CL-004 | NPA is not a practical replacement for Lean or Rocq. This boundary must stay visible beside any comparison. | Verified boundary claim | S01 / S03 / S05 / 2026-07-02 | Retain the disclaimer. |
| CL-005 | npa-std and npa-mathlib are separate public theorem-package repositories in the finitefield-org organization. | Verified public claim | S01 / S02 / 2026-07-02 | Recheck repository visibility again if publication is delayed or repositories change. |
| CL-006 | The npa, npa-std, and npa-mathlib repositories each expose Apache-2.0 licensing through their public LICENSE metadata. | Verified public claim | S01 / S02 / 2026-07-02 | Recheck LICENSE on a major release. |
Repositories and license
Keep code, package repositories, and organization visibility explicit.
Repository links are public-source pointers, not guarantees that the current page is synchronized with the latest GitHub state.
4 repositories shown
finitefield-org
npa
Certificate-first proof assistance and verification toolchain.
- License
- Apache-2.0 verified from LICENSE on 2026-07-02.
- Verification
- Latest git tag: v0.2.0. No latest GitHub release is published. README current toolchain reference: NPA_GIT_TAG=v0.2.0.
experimentalRust / OCamlcertificate-first
Open repository
finitefield-org
npa-std
Standard theorem package repository for NPA proof sources.
- License
- Apache-2.0 verified from LICENSE on 2026-07-02.
- Verification
- Latest git tag and GitHub release: v0.1.0. README package metadata version: 0.1.0; package toolchain pin: NPA_GIT_TAG=v0.1.1.
experimentaltheorem packageproof source
Open repository
finitefield-org
npa-mathlib
Formal mathematics library research repository.
- License
- Apache-2.0 verified from LICENSE on 2026-07-02.
- Verification
- Latest git tag: v0.1.30. Latest GitHub release: v0.1.9. README package metadata version: 0.2.1; package toolchain pin: NPA_GIT_TAG=v0.1.1.
researchformal mathematicslibrary
Open repository
finitefield-org
Finite Field GitHub organization
Public organization snapshot for the Lab repository family.
- License
- Repository-specific licenses apply
- Verification
- npa, npa-std, and npa-mathlib are public as of the 2026-07-02 GitHub API readback.
public indexvisibility snapshotsource
Open organization
No repository matched the current search.
The GitHub repositories are the source for public code status. License, current tags, public visibility, and release wording were checked on 2026-07-02 as the M10-T14 final readback.
Proof ecosystem guard
Clarify roles before comparing proof tools.
This is a role table, not a ranking. Lean and Rocq remain the reference proof-assistant ecosystems; NPA is presented as certificate-centered research and implementation work.
| Item | Lean | Rocq | NPA |
|---|---|---|---|
| Position | Open-source programming language and proof assistant. | Interactive theorem prover with a long research history. | Research and implementation repository for certificate-first checking. |
| Typical use | Mathematics, software verification, and programming. | Mathematics, specifications, program verification, and extraction. | Research into proof certificates, independent checking, and a small trusted base. |
| Evidence boundary | Its own trusted kernel and ecosystem define the checking boundary. | Its own kernel and checked developments define the checking boundary. | The canonical .npcert artifact crosses from generation into checking. |
| How this page treats it | Reference for learning, comparison, and interoperability. | Reference for learning, comparison, and formalization methods. | Finite Field research project, not a product promise. |
| Boundary | Specialist knowledge is still required. | Specialist knowledge is still required. | NPA is not a practical replacement for Lean or Rocq at this time. |
Sources
Publish the source map beside the interpretation.
Sources are shown so the reader can tell which claims come from public repositories, official proof-tool sites, and company context.
S01
finitefield-org/npa
Primary source for NPA purpose, trust model, v0.2.0 current repository tag wording, commands, repository layout, and license.
Open source S02Finite Field GitHub organization
Primary source for public repository visibility, latest git tags, release pages, and the Lab repository family snapshot checked on 2026-07-02.
Open source S03Lean official site
Primary source for Lean's public positioning, checked on 2026-07-02.
Open source S04Lean language reference
Primary source for dependent type theory and kernel reference context, checked on 2026-07-02.
Open source S05Rocq Prover official site
Primary source for Rocq's public positioning, checked on 2026-07-02.
Open source S06FINITE FIELD company site
Company source for Finite Field brand and business context.
Open sourceFAQ
NPA status and verification boundaries.
The answers emphasize the trust boundary before readers confuse a research page with a deployed proof-assistant service.
Read about the company01 Is this page a product guarantee?
No. NPA is shown here as a research and implementation repository.
02 Can NPA replace Lean or Rocq?
No. NPA is not a practical replacement for Lean or Rocq.
03 Does the page run real NPA verification?
No. The browser simulation does not run NPA itself, Rust, WASM, or real proof certificates.
04 What counts as evidence here?
The certificate artifact, deterministic hashes, Rust kernel/verifier result, source-free reference checker result, and axiom report form the checking-side evidence.
05 Which facts need rechecking?
Current public version, repository visibility, toolchain pins, license text, and source wording were rechecked on 2026-07-02.
From proof discipline to operations
Use the same evidence discipline when a business decision must be trusted.
For business systems, the useful lesson is not to add theorem proving everywhere. It is to decide what must be generated, checked, logged, corrected, and approved by people.