NPA / Preverjanje dokazov, ki najprej uporablja certifikate

NPA: izpostavite mejo dokaznih evidenc, preden zaupate rezultatu.

Ta stran odsek NPA iz matematičnega laboratorija preoblikuje v samostojno dokazno stran: javno stanje, model zaupanja, dokazni cevovod, register trditev, repozitorije, vire in izrecno besedilo, da NPA ni zamenjava.

Preglejte mejo zaupanja Odprite repozitorij GitHub

Javno stanje: Raziskovalni repozitorij; Prikazano kot raziskave in izvedba, ne kot produkcijska storitev zagotavljanja.
Javno ponovno preverjanje: 2026-07-02 / NPA v0.2.0; Preverjene najnovejše oznake git: npa v0.2.0, npa-std v0.1.0, npa-mathlib v0.1.30.
Licenca: Apache-2.0; Apache-2.0 je bil 2026-07-02 preverjen za npa, npa-std in npa-mathlib.

Javno ponovno preverjanje: 2026-07-02. Najnovejša oznaka git repozitorija NPA je v0.2.0; npa-std je v0.1.0; npa-mathlib je v0.1.30. Pripete različice v README-jih paketov so prikazane kot kontekst posameznih repozitorijev in niso združene v eno trditev o različici NPA.

Predogled strani z dokazi NPA, ki prikazuje preverjanje certifikatov in pregled meje zaupanja — Vizual je statični predogled rezultata preverjanja certifikata in pojasnila o meji zaupanja. To ni živa sled NPA.

Javno stanje

Povejte, kaj je javno, kaj je dokaz in kdaj je bilo ponovno preverjeno.

Ta stran razkriva podlago strani: lokalni posnetek resničnosti, javni vir repozitorija in datum končnega predzagonskega odčitka.

Javno stanje

Raziskovalni in izvedbeni repozitorij

Repozitorij GitHub je javen, vendar ta stran opisuje raziskovalni in izvedbeni repozitorij, ne uvedene storitve.

Javno ponovno preverjanje

2026-07-02

Odčitek javnega vira je bil opravljen 2026-07-02. Prvotna rekonstrukcija vira še vedno uporablja lokalni posnetek resničnosti z dne 2026-06-21.

Dokazi

Certifikati in zgoščene vrednosti

Posnetek vira beleži kanonični .npcert, certificate_hash, export_hash, axiom_report_hash in odločitve preverjevalnika.

Licenca

Apache-2.0 preverjen

Apache-2.0 je bil 2026-07-02 preverjen za npa, npa-std in npa-mathlib prek javnih metapodatkov LICENSE.

Meja

NPA ni praktična zamenjava za Lean ali Rocq. Razdeljena simulacija pregleda v brskalniku ne izvaja samega NPA. Javne oznake, licenca in vidnost repozitorijev so bili za končni predobjavni odčitek preverjeni 2026-07-02.

Meja zaupanja

Čez dokazno mejo premaknite samo kanonični certifikat.

Meja ni odvisna od tega, katero orodje je videti izpopolnjeno. Pomembno je, kateri artefakt sme po neodvisnem preverjanju postati dokaz.

Razčlenjevalnik, elaborator, taktike, avtomatizacija, iskanje izrekov, vtičniki, sistemi AI, izvorne datoteke, datoteke ponovnega predvajanja, indeksi izrekov, načrti objave, stanje CI, strani izdaj in metapodatki registra ostanejo na nezaupanja vredni strani kandidatov.

Dokazni cevovod / pojasnjevalna simulacija

Prikažite natančen cevovod od bajtov certifikata do dokazov preverjanja.

Simulacija v brskalniku ne izvaja samega NPA, Rusta, WASM ali pravih dokaznih certifikatov. Prikazuje vrstni red preverjanja brez izvorne kode, ki ga morajo zadovoljiti pravi artefakti.

Pot dokazov CLI

npa package verify-certs --root . --checker reference --json

NPA / revizijska sled PRIPRAVLJENO

01 Format certifikatakanonični bajti .npcert / razčlenljiv certifikat / preverjanje formata ČAKA
02 Zgoščena vrednost certifikatabajti certifikata / certificate_hash / deterministični povzetek ČAKA
03 Odločitev jedracertifikat / sprejmi ali zavrni / poročilo preverjevalnika v Rustu ČAKA
04 Referenčni preverjevalnikcertifikat, pripet z zgoščeno vrednostjo / neodvisno sprejmi ali zavrni / poročilo preverjevalnika brez izvorne kode ČAKA
05 Poročilo o aksiomihpreverjeni paket / axiom_report_hash / popis predpostavk ČAKA

Odločitev

Pojasnjevalni cevovod še ni zagnan.

Zaženite pojasnilo, da se pot preverjanja brez izvorne kode označi po vrstnem redu.

Ločite dokaze, časovno občutljiva dejstva in mejne trditve.

Stran ne temelji na ohlapnem raziskovalnem besedilu. Vsaka javna izjava je povezana z lokalnim posnetkom resničnosti, virom in ukrepom ob objavi.

Trditev	Javno besedilo	Stanje	Vir	Ukrep ob objavi
CL-001	NPA najprej uporablja certifikate: meja za revizijo je kanonični artefakt .npcert in pot preverjanja okoli njega.	Preverjena javna trditev	S01 / 2026-07-02	Preglejte ob spremembi README.
CL-002	Javno ponovno preverjanje 2026-07-02 je v repozitoriju NPA našlo najnovejšo oznako git v0.2.0. README-ji povezanih paketov še vedno kažejo na repozitorijsko določene različice, zato besedilo o različici ostaja omejeno na posamezen repozitorij.	Preverjeno javno ponovno preverjanje	S01 / S02 / 2026-07-02	Besedilo o oznakah naj ostane omejeno na repozitorij.
CL-003	Lokalni posnetek resničnosti beleži pripeto orodno verigo Rust 1.95.0; to ni uporabljeno kot trženjska trditev.	Preverjeno, časovno občutljivo	S01 / 2026-07-02	Ponovno preverite, če je prikazana različica orodne verige.
CL-004	NPA ni praktična zamenjava za Lean ali Rocq. Ta meja mora ostati vidna ob vsaki primerjavi.	Preverjena mejna trditev	S01 / S03 / S05 / 2026-07-02	Ohranite pojasnilo o omejitvi.
CL-005	npa-std in npa-mathlib sta ločena javna repozitorija paketov izrekov v organizaciji finitefield-org.	Preverjena javna trditev	S01 / S02 / 2026-07-02	Ponovno preverite vidnost repozitorijev, če se objava zamakne ali se repozitoriji spremenijo.
CL-006	Repozitoriji npa, npa-std in npa-mathlib prek javnih metapodatkov LICENSE prikazujejo licenco Apache-2.0.	Preverjena javna trditev	S01 / S02 / 2026-07-02	Ob večji izdaji ponovno preverite LICENSE.

Repozitoriji in licenca

Jasno prikažite kodo, paketne repozitorije in vidnost organizacije.

Povezave do repozitorijev so kazalci na javne vire, ne jamstva, da je trenutna stran usklajena z najnovejšim stanjem na GitHubu.

4 prikazani repozitoriji

finitefield-org

npa

Orodna veriga za dokazovalno pomoč in preverjanje, ki najprej uporablja certifikate.

Licenca: Apache-2.0 preverjen iz LICENSE 2026-07-02.
Preverjanje: Najnovejša oznaka git: v0.2.0. Najnovejša izdaja GitHub ni objavljena. Trenutna referenca orodne verige v README: NPA_GIT_TAG=v0.2.0.

eksperimentalnoRust / OCamlnajprej certifikati

Odpri repozitorij

finitefield-org

npa-std

Repozitorij standardnega paketa izrekov za dokazne vire NPA.

Licenca: Apache-2.0 preverjen iz LICENSE 2026-07-02.
Preverjanje: Najnovejša oznaka git in izdaja GitHub: v0.1.0. Metapodatkovna različica paketa v README: 0.1.0; pripeta orodna veriga paketa: NPA_GIT_TAG=v0.1.1.

eksperimentalnopaket izrekovdokazni vir

Odpri repozitorij

finitefield-org

npa-mathlib

Raziskovalni repozitorij knjižnice formalne matematike.

Licenca: Apache-2.0 preverjen iz LICENSE 2026-07-02.
Preverjanje: Najnovejša oznaka git: v0.1.30. Najnovejša izdaja GitHub: v0.1.9. Metapodatkovna različica paketa v README: 0.2.1; pripeta orodna veriga paketa: NPA_GIT_TAG=v0.1.1.

raziskaveformalna matematikaknjižnica

Odpri repozitorij

finitefield-org

Organizacija Finite Field na GitHubu

Javni posnetek organizacije za družino repozitorijev laboratorija.

Licenca: Veljajo licence posameznih repozitorijev
Preverjanje: npa, npa-std in npa-mathlib so javni glede na odčitek GitHub API z dne 2026-07-02.

javni indeksposnetek vidnostivir

Odpri organizacijo

Repozitoriji GitHub so vir za javno stanje kode. Licenca, trenutne oznake, javna vidnost in besedilo o izdajah so bili preverjeni 2026-07-02 kot končni odčitek M10-T14.

Varovalo ekosistema dokazov

Razjasnite vloge, preden primerjate orodja za dokaze.

To je tabela vlog, ne lestvica. Lean in Rocq ostajata referenčna ekosistema dokazovalnih pomočnikov; NPA je predstavljen kot raziskovalno in izvedbeno delo, osredotočeno na certifikate.

Postavka	Lean	Rocq	NPA
Položaj	Odprtokodni programski jezik in dokazovalni pomočnik.	Interaktivni dokazovalnik izrekov z dolgo raziskovalno zgodovino.	Raziskovalni in izvedbeni repozitorij za preverjanje, ki najprej uporablja certifikate.
Tipična uporaba	Matematika, preverjanje programske opreme in programiranje.	Matematika, specifikacije, preverjanje programov in ekstrakcija.	Raziskave dokaznih certifikatov, neodvisnega preverjanja in majhne zaupanja vredne osnove.
Meja dokazov	Njegovo lastno zaupanja vredno jedro in ekosistem določata mejo preverjanja.	Njegovo lastno jedro in preverjeni razvoj določata mejo preverjanja.	Kanonični artefakt .npcert preide iz generiranja v preverjanje.
Kako ga obravnava ta stran	Referenca za učenje, primerjavo in interoperabilnost.	Referenca za učenje, primerjavo in metode formalizacije.	Raziskovalni projekt Finite Field, ne obljuba izdelka.
Meja	Še vedno je potrebno specialistično znanje.	Še vedno je potrebno specialistično znanje.	NPA trenutno ni praktična zamenjava za Lean ali Rocq.

Uradno spletno mesto Lean Uradno spletno mesto Rocq Prover NPA na GitHubu

Viri

Objavite zemljevid virov ob interpretaciji.

Viri so prikazani, da bralec vidi, katere trditve izhajajo iz javnih repozitorijev, uradnih spletnih mest dokazovalnih orodij in konteksta podjetja.

S01

finitefield-org/npa

Primarni vir za namen NPA, model zaupanja, besedilo trenutne oznake repozitorija v0.2.0, ukaze, strukturo repozitorija in licenco.

Odpri vir S02

Organizacija Finite Field na GitHubu

Primarni vir za vidnost javnih repozitorijev, najnovejše oznake git, strani izdaj in posnetek družine repozitorijev laboratorija, preverjen 2026-07-02.

Odpri vir S03

Uradno spletno mesto Lean

Primarni vir za javno pozicioniranje Leana, preverjen 2026-07-02.

Odpri vir S04

Referenca jezika Lean

Primarni vir za teorijo odvisnih tipov in kontekst reference jedra, preverjen 2026-07-02.

Odpri vir S05

Uradno spletno mesto Rocq Prover

Primarni vir za javno pozicioniranje Rocqa, preverjen 2026-07-02.

Odpri vir S06

Spletno mesto podjetja FINITE FIELD

Vir podjetja za znamko Finite Field in poslovni kontekst.

Odpri vir

Pogosta vprašanja

Stanje NPA in meje preverjanja.

Odgovori poudarjajo mejo zaupanja, preden bi bralci raziskovalno stran zamenjali za uvedeno storitev dokazovalnega pomočnika.

Preberite o podjetju

01 Ali je ta stran jamstvo za izdelek?

Ne. NPA je tukaj prikazan kot raziskovalni in izvedbeni repozitorij.

02 Ali lahko NPA nadomesti Lean ali Rocq?

Ne. NPA ni praktična zamenjava za Lean ali Rocq.

03 Ali stran izvaja pravo preverjanje NPA?

Ne. Simulacija v brskalniku ne izvaja samega NPA, Rusta, WASM ali pravih dokaznih certifikatov.

04 Kaj se tukaj šteje za dokaz?

Certifikatni artefakt, deterministične zgoščene vrednosti, rezultat jedra oziroma preverjevalnika v Rustu, rezultat referenčnega preverjevalnika brez izvorne kode in poročilo o aksiomih tvorijo dokaze na strani preverjanja.

05 Katera dejstva je treba znova preveriti?

Trenutna javna različica, vidnost repozitorijev, pripete različice orodne verige, licenčno besedilo in besedilo virov so bili ponovno preverjeni 2026-07-02.

Od dokazne discipline do poslovanja

Uporabite enako disciplino dokazov, kadar mora biti poslovna odločitev zaupanja vredna.

Za poslovne sisteme koristna lekcija ni, da bi povsod dodajali dokazovanje izrekov. Gre za odločitev, kaj je treba generirati, preveriti, zapisati v dnevnik, popraviti in dati ljudem v odobritev.

Preverite poslovno vprašanje Oglejte si prototip