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: make the proof-evidence boundary explicit before trusting a result.
This standalone page brings together the NPA material from Math Lab. It explains what is public, how trust is established, how proofs are checked, which claims are supported, where the source repositories are, and why NPA is not a replacement for existing proof assistants.
- 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 counts as evidence, and when each was last checked.
This page shows the evidence behind its claims, the public sources used, and when they were last checked.
Public recheck
2026-07-02
The public sources were rechecked on 2026-07-02. This page also cites the reviewed 2026-06-21 source snapshot where relevant.
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 from their public LICENSE files on 2026-07-02.
Boundary
NPA is not a practical replacement for Lean or Rocq. The browser-based inspection simulation does not run NPA itself. Public tags, license, and repository visibility were checked on 2026-07-02.
Trust boundary
Let only a canonical certificate cross the evidence boundary.
The boundary is not defined by how sophisticated a tool appears. It is defined by which artifact may count as 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
Trace the exact path from certificate bytes to independently checkable evidence.
The browser simulation does not run NPA, Rust, WebAssembly, or actual proof certificates. It illustrates the source-independent sequence of checks that real artifacts must pass.
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
Distinguish evidence from time-sensitive facts and claims about scope.
Rather than relying on vague descriptions of the research, the page links every public claim to a reviewed snapshot, a source, and the action required before publication.
| 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 reviewed source 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 publish an Apache-2.0 LICENSE file. | Verified public claim | S01 / S02 / 2026-07-02 | Recheck LICENSE on a major release. |
Repositories and license
Show the code repositories, package repositories, and publishing organizations clearly.
Repository links point to public sources; they do not guarantee that this page matches the latest state on GitHub.
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 GitHub release has been published for v0.2.0. 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.
Proof ecosystem context
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
Show each interpretation alongside its sources.
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's 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.