NPA / sertifikaadikeskne tõestuste kontrollimine

NPA: näita tõenduspiiri enne tulemuse usaldamist.

See leht esitab Math Labi NPA jaotise iseseisva tõenduslehena: avalik olek, usaldusmudel, tõestuskonveier, väidete register, hoidlad, allikad ja selge märkus, et NPA ei ole Leani ega Rocqi asendus.

Uuri usalduspiiri Ava GitHubi hoidla

Avalik olek: Uurimis- ja teostushoidla; Esitatud uurimis- ja teostustööna, mitte tootmiskindluse teenusena.
Avalik korduskontroll: 2026-07-02 / NPA v0.2.0; Kontrollitud uusimad git-sildid: npa v0.2.0, npa-std v0.1.0, npa-mathlib v0.1.30.
Litsents: Apache-2.0; Apache-2.0 kontrolliti npa, npa-std ja npa-mathlib jaoks 2026-07-02.

Avalik korduskontroll: 2026-07-02. NPA hoidla uusim git-silt on v0.2.0; npa-std on v0.1.0; npa-mathlib on v0.1.30. Pakettide README-s kinnitatud versioone näidatakse hoidlakohase kontekstina ja neid ei ühendata üheks NPA versiooniväiteks.

NPA tõenduslehe eelvaade, kus on sertifikaadikontroll ja usalduspiiri ülevaatus — Visuaal on sertifikaadikontrolli tulemuse ja usalduspiiri selgituse staatiline eelvaade. See ei ole NPA reaalajas jälg.

Avalik olek

Ütle, mis on avalik, mis on tõendus ja millal seda uuesti kontrolliti.

See leht teeb nähtavaks oma aluse: kohaliku tõehetktõmmise, avaliku hoidla allika ja lõpliku käivituseelse korduslugemise kuupäeva.

Avalik olek

Uurimis- ja teostushoidla

GitHubi hoidla on avalik, kuid see leht kirjeldab uurimis- ja teostushoidlat, mitte kasutusele võetud teenust.

Avalik korduskontroll

2026-07-02

Avalike allikate korduslugemine lõpetati 2026-07-02. Algne allika rekonstruktsioon kasutab endiselt 2026-06-21 kohalikku tõehetktõmmist.

Tõendus

Sertifikaadid ja räsid

Allikahetktõmmis talletab kanoonilise .npcert artefakti, certificate_hash, export_hash, axiom_report_hash ja kontrollija otsused.

Litsents

Apache-2.0 kontrollitud

Apache-2.0 kontrolliti npa, npa-std ja npa-mathlib jaoks avalike LICENSE-metaandmete kaudu 2026-07-02.

Piir

NPA ei ole Leani ega Rocqi praktiline asendus. Hajutatud brauseri kontrollisimulatsioon ei käivita NPA-d ennast. Avalikud sildid, litsents ja hoidla nähtavus kontrolliti 2026-07-02 lõpliku avaldamise korduslugemise jaoks.

Usalduspiir

Liiguta tõenduspiirist üle ainult kanooniline sertifikaat.

Piir ei sõltu sellest, milline tööriist paistab keerukam. Oluline on, millisel artefaktil lubatakse pärast sõltumatut kontrolli tõenduseks saada.

Parser, elaboraator, taktikad, automatiseerimine, teoreemiotsing, pluginad, AI-süsteemid, lähtefailid, taasesitusfailid, teoreemiindeksid, avaldamisplaanid, CI olek, väljalaskelehed ja registri metaandmed jäävad usaldamata kandidaadipoolele.

Tõestuskonveier / selgitav simulatsioon

Näita täpset konveierit sertifikaadibaitidest kontrollitõenduseni.

Brauserisimulatsioon ei käivita NPA-d ennast, Rusti, WASMi ega tegelikke tõestussertifikaate. See visualiseerib lähtekoodivaba kontrollijärjekorda, millele tegelikud artefaktid peavad vastama.

CLI tõendustee

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

NPA / auditijälg VALMIS

01 Sertifikaadi vormingkanoonilised .npcert baidid / parsitav sertifikaat / vormingu kontroll OOTEL
02 Sertifikaadi räsisertifikaadibaidid / certificate_hash / deterministlik räsi OOTEL
03 Tuuma otsussertifikaat / vastu võtta või tagasi lükata / Rusti verifitseerija aruanne OOTEL
04 Võrdluskontrollijaräsiga kinnitatud sertifikaat / sõltumatu vastuvõtmine või tagasilükkamine / lähtekoodivaba kontrollija aruanne OOTEL
05 Aksioomiaruannekontrollitud pakett / axiom_report_hash / eelduste inventuur OOTEL

Otsus

Selgitavat konveierit pole veel käivitatud.

Käivita selgitus, et märkida lähtekoodivaba kontrollitee järjekorras.

Väidete register

Eralda tõendus, ajatundlikud faktid ja piiriväited.

Leht ei tugine ebamäärasele uurimistekstile. Iga avalik väide on seotud kohaliku tõehetktõmmise, allika ja avaldamistoiminguga.

Väide	Avalik sõnastus	Olek	Allikas	Avaldamistoiming
CL-001	NPA on sertifikaadikeskne: auditeeritav piir on kanooniline .npcert artefakt ja seda ümbritsev kontrollitee.	Kontrollitud avalik väide	S01 / 2026-07-02	Vaata üle, kui README muutub.
CL-002	2026-07-02 avalik korduskontroll leidis, et NPA hoidla uusim git-silt on v0.2.0. Seotud pakettide README-d näitavad endiselt hoidlakohaseid kinnitatud versioone, mistõttu versioonisõnastus jääb hoidla piiresse.	Kontrollitud avalik korduskontroll	S01 / S02 / 2026-07-02	Hoia sildi sõnastus hoidla piires.
CL-003	Kohalik tõehetktõmmis talletab Rust 1.95.0 tööriistaahela kinnitatud versiooni; seda ei kasutata turundusväitena.	Kontrollitud, ajatundlik	S01 / 2026-07-02	Kontrolli uuesti, kui tööriistaahela versiooni kuvatakse.
CL-004	NPA ei ole Leani ega Rocqi praktiline asendus. See piir peab jääma nähtavaks iga võrdluse kõrval.	Kontrollitud piiriväide	S01 / S03 / S05 / 2026-07-02	Säilita lahtiütlus.
CL-005	npa-std ja npa-mathlib on finitefield-org organisatsiooni eraldi avalikud teoreemipakettide hoidlad.	Kontrollitud avalik väide	S01 / S02 / 2026-07-02	Kontrolli hoidlate nähtavust uuesti, kui avaldamine viibib või hoidlad muutuvad.
CL-006	Hoidlad npa, npa-std ja npa-mathlib avaldavad igaüks Apache-2.0 litsentsi oma avalike LICENSE-metaandmete kaudu.	Kontrollitud avalik väide	S01 / S02 / 2026-07-02	Kontrolli LICENSE suure väljalaske korral uuesti.

Hoidlad ja litsents

Hoia kood, paketihoidlad ja organisatsiooni nähtavus selged.

Hoidlate lingid viitavad avalikele allikatele, kuid ei garanteeri, et leht on GitHubi uusima olekuga sünkroonis.

4 hoidlat

finitefield-org

npa

Sertifikaadikeskne tõestusabi ja verifitseerimise tööriistaahel.

Litsents: Apache-2.0 kontrolliti LICENSE põhjal 2026-07-02.
Kontroll: Uusim git-silt: v0.2.0. Uusimat GitHubi väljalaset ei ole avaldatud. README praegune tööriistaahela viide: NPA_GIT_TAG=v0.2.0.

eksperimentaalneRust / OCamlsertifikaadikeskne

Ava hoidla

finitefield-org

npa-std

NPA tõestusallikate standardne teoreemipaketi hoidla.

Litsents: Apache-2.0 kontrolliti LICENSE põhjal 2026-07-02.
Kontroll: Uusim git-silt ja GitHubi väljalase: v0.1.0. README paketi metaandmete versioon: 0.1.0; paketi tööriistaahela kinnitatud versioon: NPA_GIT_TAG=v0.1.1.

eksperimentaalneteoreemipaketttõestusallikas

Ava hoidla

finitefield-org

npa-mathlib

Formaalse matemaatika teegi uurimishoidla.

Litsents: Apache-2.0 kontrolliti LICENSE põhjal 2026-07-02.
Kontroll: Uusim git-silt: v0.1.30. Uusim GitHubi väljalase: v0.1.9. README paketi metaandmete versioon: 0.2.1; paketi tööriistaahela kinnitatud versioon: NPA_GIT_TAG=v0.1.1.

uurimusformaalne matemaatikateek

Ava hoidla

finitefield-org

Finite Fieldi GitHubi organisatsioon

Avalik organisatsiooni hetktõmmis Labi hoidlate perekonnale.

Litsents: Kehtivad hoidlakohased litsentsid
Kontroll: npa, npa-std ja npa-mathlib on 2026-07-02 GitHub API korduslugemise järgi avalikud.

avalik indeksnähtavuse hetktõmmisallikas

Ava organisatsioon

GitHubi hoidlad on avaliku koodi oleku allikas. Litsentsi, praeguseid silte, avalikku nähtavust ja väljalaske sõnastust kontrolliti 2026-07-02 M10-T14 lõpliku korduslugemisena.

Tõestusökosüsteemi piir

Selgita rolle enne tõestustööriistade võrdlemist.

See on rollitabel, mitte pingerida. Lean ja Rocq jäävad tõestusassistentide võrdlusökosüsteemideks; NPA-d esitletakse sertifikaadikeskse uurimis- ja teostustööna.

Üksus	Lean	Rocq	NPA
Asend	Avatud lähtekoodiga programmeerimiskeel ja tõestusassistent.	Pika uurimisajalooga interaktiivne teoreemitõestaja.	Uurimis- ja teostushoidla sertifikaadikeskseks kontrollimiseks.
Tüüpiline kasutus	Matemaatika, tarkvara verifitseerimine ja programmeerimine.	Matemaatika, spetsifikatsioonid, programmide verifitseerimine ja eraldamine.	Tõestussertifikaatide, sõltumatu kontrolli ja väikese usaldatud aluse uurimine.
Tõenduspiir	Selle enda usaldatud tuum ja ökosüsteem määravad kontrollipiiri.	Selle enda tuum ja kontrollitud arendused määravad kontrollipiiri.	Kanooniline .npcert artefakt liigub genereerimisest kontrolli.
Kuidas see leht seda käsitleb	Õppimise, võrdluse ja koostalitluse lähtekoht.	Õppimise, võrdluse ja formaliseerimismeetodite lähtekoht.	Finite Fieldi uurimisprojekt, mitte tootelubadus.
Piir	Eriteadmised on endiselt vajalikud.	Eriteadmised on endiselt vajalikud.	NPA ei ole praegu Leani ega Rocqi praktiline asendus.

Leani ametlik sait Rocq Proveri ametlik sait NPA GitHub

Allikad

Avalda allikakaart tõlgenduse kõrval.

Allikaid näidatakse, et lugeja eristaks avalikest hoidlatest, ametlikelt tõestustööriistade saitidelt ja ettevõtte kontekstist pärinevaid väiteid.

S01

finitefield-org/npa

Esmane allikas NPA eesmärgi, usaldusmudeli, praeguse hoidla v0.2.0 sildisõnastuse, käskude, hoidla struktuuri ja litsentsi kohta.

Ava allikas S02

Finite Fieldi GitHubi organisatsioon

Esmane allikas avalike hoidlate nähtavuse, uusimate git-siltide, väljalaskelehtede ja 2026-07-02 kontrollitud Labi hoidlate perekonna hetktõmmise kohta.

Ava allikas S03

Leani ametlik sait

Esmane allikas Leani avaliku positsiooni kohta, kontrollitud 2026-07-02.

Ava allikas S04

Leani keele viide

Esmane allikas sõltuvate tüüpide teooria ja tuuma võrdluskonteksti kohta, kontrollitud 2026-07-02.

Ava allikas S05

Rocq Proveri ametlik sait

Esmane allikas Rocqi avaliku positsiooni kohta, kontrollitud 2026-07-02.

Ava allikas S06

Finite Fieldi ettevõtte sait

Ettevõtte allikas Finite Fieldi kaubamärgi ja ärikonteksti jaoks.

Ava allikas

KKK

NPA olek ja verifitseerimispiirid.

Vastused rõhutavad usalduspiiri enne, kui lugejad ajavad uurimislehe segi kasutusele võetud tõestusassistendi teenusega.

Loe ettevõtte kohta

01 Kas see leht on tootegarantii?

Ei. NPA-d näidatakse siin uurimis- ja teostushoidlana.

02 Kas NPA saab Leani või Rocqi asendada?

Ei. NPA ei ole Leani ega Rocqi praktiline asendus.

03 Kas leht käivitab tegeliku NPA verifitseerimise?

Ei. Brauserisimulatsioon ei käivita NPA-d ennast, Rusti, WASMi ega tegelikke tõestussertifikaate.

04 Mida siin tõenduseks loetakse?

Sertifikaadiartefakt, deterministlikud räsid, Rusti tuuma/verifitseerija tulemus, lähtekoodivaba võrdluskontrollija tulemus ja aksioomiaruanne moodustavad kontrollipoole tõenduse.

05 Millised faktid vajavad korduskontrolli?

Praegust avalikku versiooni, hoidla nähtavust, tööriistaahela kinnitatud versioone, litsentsiteksti ja allika sõnastust kontrolliti uuesti 2026-07-02.

Tõestusdistsipliinist töökorralduseni

Kasuta sama tõendusdistsipliini, kui äriotsust peab saama usaldada.

Ärisüsteemides ei ole kasulik õppetund lisada teoreemitõestamist kõikjale. Tuleb otsustada, mida inimesed peavad genereerima, kontrollima, logima, parandama ja heaks kiitma.

Kontrolli äriprobleemi Vaata prototüüpi