NPA / Sertifikaatit ensin -todistusten tarkistus

NPA: tuo todistusnäytön raja näkyviin ennen tulokseen luottamista.

Tämä sivu rakentaa Math Labin NPA-osion erilliseksi näyttösivuksi: julkinen tila, luottamusmalli, todistusputki, väiterekisteri, repositoriot, lähteet ja selkeä sanamuoto siitä, ettei NPA ole korvaaja.

Tarkastele luottamusrajaa Avaa GitHub-repositorio

Julkinen tila: Tutkimusrepositorio; Esitetään tutkimuksena ja toteutuksena, ei tuotantovarmennuspalveluna.
Julkinen uudelleentarkistus: 2026-07-02 / NPA v0.2.0; Uusimmat git-tagit tarkistettu: npa v0.2.0, npa-std v0.1.0, npa-mathlib v0.1.30.
Lisenssi: Apache-2.0; Apache-2.0 tarkistettiin npa-, npa-std- ja npa-mathlib-repositorioille 2026-07-02.

Julkinen uudelleentarkistus: 2026-07-02. NPA-repositorion uusin git-tagi on v0.2.0; npa-std on v0.1.0; npa-mathlib on v0.1.30. Pakettien README-kiinnitykset näytetään repositoriokohtaisena kontekstina eikä niitä yhdistetä yhdeksi NPA-version väitteeksi.

NPA:n näyttösivun esikatselu, jossa näkyvät sertifikaatin tarkistus ja luottamusrajan tarkastelu — Kuva on staattinen esikatselu sertifikaatin tarkistustuloksesta ja luottamusrajan selityksestä. Se ei ole reaaliaikainen NPA-jälki.

Julkinen tila

Kerro, mikä on julkista, mikä on näyttöä ja milloin se tarkistettiin uudelleen.

Tämä sivu tekee sivun perustan näkyväksi: paikallinen totuustilannekuva, julkinen repositoriolähde ja viimeinen julkaisua edeltävä tarkistuspäivä.

Julkinen tila

Tutkimus- ja toteutusrepositorio

GitHub-repositorio on julkinen, mutta tämä sivu kuvaa tutkimus- ja toteutusrepositoriota, ei käyttöönotettua palvelua.

Julkinen uudelleentarkistus

2026-07-02

Julkisten lähteiden tarkistus valmistui 2026-07-02. Alkuperäinen lähteen rekonstruointi käyttää edelleen paikallista totuustilannekuvaa 2026-06-21.

Näyttö

Sertifikaatit ja tiivisteet

Lähdetilannekuva kirjaa kanonisen .npcert-artefaktin, certificate_hash-, export_hash- ja axiom_report_hash-arvot sekä tarkistinten ratkaisut.

Lisenssi

Apache-2.0 tarkistettu

Apache-2.0 tarkistettiin npa-, npa-std- ja npa-mathlib-repositorioille julkisen LICENSE-metadatan kautta 2026-07-02.

Raja

NPA ei ole käytännön korvaaja Leanille tai Rocqille. Julkaistu selaintarkastelun simulaatio ei aja NPA:ta itseään. Julkiset tagit, lisenssi ja repositorioiden näkyvyys tarkistettiin 2026-07-02 julkaisua edeltävää lopputarkistusta varten.

Luottamusraja

Siirrä näyttörajan yli vain kanoninen sertifikaatti.

Raja ei koske sitä, mikä työkalu näyttää kehittyneeltä. Kyse on siitä, mikä artefakti saa muuttua näytöksi riippumattoman tarkistuksen jälkeen.

Jäsennin, elaboroija, taktiikat, automaatio, teoreemahaku, liitännäiset, tekoälyjärjestelmät, lähdetiedostot, uudelleentoistotiedostot, teoreemaindeksit, julkaisusuunnitelmat, CI-tila, julkaisusivut ja rekisterimetadata pysyvät ei-luotetulla ehdokaspuolella.

Todistusputki / selittävä simulaatio

Näytä tarkka putki sertifikaatin tavuista tarkistusnäyttöön.

Selainpohjainen simulaatio ei aja NPA:ta, Rustia, WASMia tai oikeita todistussertifikaatteja. Se visualisoi lähteestä riippumattoman tarkistusjärjestyksen, joka oikeiden artefaktien on täytettävä.

CLI-näyttöpolku

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

NPA / auditointijälki VALMIS

01 Sertifikaatin muotokanoniset .npcert-tavut / jäsennettävä sertifikaatti / muototarkistus ODOTA
02 Sertifikaatin tiivistesertifikaatin tavut / certificate_hash / deterministinen tiiviste ODOTA
03 Ytimen ratkaisusertifikaatti / hyväksy tai hylkää / Rust-verifioijan raportti ODOTA
04 Vertailutarkistintiivisteellä kiinnitetty sertifikaatti / riippumaton hyväksyntä tai hylkäys / lähteestä riippumattoman tarkistimen raportti ODOTA
05 Aksioomaraporttitarkistettu paketti / axiom_report_hash / oletusten inventaario ODOTA

Tulos

Selittävä putki ei ole vielä käynnistynyt.

Aja selitys, jotta lähteestä riippumaton tarkistuspolku merkitään järjestyksessä.

Väiterekisteri

Erota näyttö, aikaan sidotut faktat ja rajaväitteet.

Sivu ei nojaa väljiin tutkimusväitteisiin. Jokainen julkinen lausuma liitetään paikalliseen totuustilannekuvaan, lähteeseen ja julkaisutoimeen.

Väite	Julkinen sanamuoto	Tila	Lähde	Julkaisutoimi
CL-001	NPA on sertifikaatit ensin -malli: auditoitava raja on kanoninen .npcert-artefakti ja sitä ympäröivä tarkistuspolku.	Vahvistettu julkinen väite	S01 / 2026-07-02	Tarkista uudelleen, kun README muuttuu.
CL-002	Vuoden 2026-07-02 julkisessa uudelleentarkistuksessa NPA-repositorion uusin git-tagi oli v0.2.0. Liittyvien pakettien README-tiedostot näyttävät edelleen repositoriokohtaiset kiinnitykset, joten versiota koskeva sanamuoto pidetään repositoriokohtaisena.	Vahvistettu julkinen uudelleentarkistus	S01 / S02 / 2026-07-02	Pidä tagia koskeva sanamuoto repositoriokohtaisena.
CL-003	Paikallinen totuustilannekuva kirjaa Rust 1.95.0 -työkaluketjun kiinnityksen; sitä ei käytetä markkinointiväitteenä.	Vahvistettu, aikaan sidottu	S01 / 2026-07-02	Tarkista uudelleen, jos työkaluketjun versio näytetään.
CL-004	NPA ei ole käytännön korvaaja Leanille tai Rocqille. Tämän rajan on pysyttävä näkyvissä kaikissa vertailuissa.	Vahvistettu rajaväite	S01 / S03 / S05 / 2026-07-02	Säilytä vastuuvapauslauseke.
CL-005	npa-std ja npa-mathlib ovat erillisiä julkisia teoreemapakettien repositorioita finitefield-org-organisaatiossa.	Vahvistettu julkinen väite	S01 / S02 / 2026-07-02	Tarkista repositorioiden näkyvyys uudelleen, jos julkaisu viivästyy tai repositoriot muuttuvat.
CL-006	npa-, npa-std- ja npa-mathlib-repositoriot näyttävät Apache-2.0-lisenssin julkisen LICENSE-metadatan kautta.	Vahvistettu julkinen väite	S01 / S02 / 2026-07-02	Tarkista LICENSE uudelleen suuren julkaisun yhteydessä.

Repositoriot ja lisenssi

Pidä koodi, pakettirepositoriot ja organisaation näkyvyys selvästi näkyvillä.

Repositoriolinkit ovat julkisia lähdeviitteitä, eivät takuita siitä, että nykyinen sivu on synkronoitu uusimpaan GitHub-tilaan.

4 repositoriota näytetään

finitefield-org

npa

Sertifikaatit ensin -todistusavustus ja verifioinnin työkaluketju.

Lisenssi: Apache-2.0 tarkistettu LICENSE-tiedostosta 2026-07-02.
Verifiointi: Uusin git-tagi: v0.2.0. Uusinta GitHub-julkaisua ei ole julkaistu. README:n nykyinen työkaluketjuviite: NPA_GIT_TAG=v0.2.0.

kokeellinenRust / OCamlsertifikaatit ensin

Avaa repositorio

finitefield-org

npa-std

NPA:n todistuslähteiden vakioteoreemapakettien repositorio.

Lisenssi: Apache-2.0 tarkistettu LICENSE-tiedostosta 2026-07-02.
Verifiointi: Uusin git-tagi ja GitHub-julkaisu: v0.1.0. README:n pakettimetadatan versio: 0.1.0; paketin työkaluketjun kiinnitys: NPA_GIT_TAG=v0.1.1.

kokeellinenteoreemapakettitodistuslähde

Avaa repositorio

finitefield-org

npa-mathlib

Formaalin matematiikkakirjaston tutkimusrepositorio.

Lisenssi: Apache-2.0 tarkistettu LICENSE-tiedostosta 2026-07-02.
Verifiointi: Uusin git-tagi: v0.1.30. Uusin GitHub-julkaisu: v0.1.9. README:n pakettimetadatan versio: 0.2.1; paketin työkaluketjun kiinnitys: NPA_GIT_TAG=v0.1.1.

tutkimusformaali matematiikkakirjasto

Avaa repositorio

finitefield-org

Finite Fieldin GitHub-organisaatio

Julkinen organisaatiotilannekuva Lab-repositorioperheelle.

Lisenssi: Repositoriokohtaiset lisenssit ovat voimassa
Verifiointi: npa, npa-std ja npa-mathlib ovat julkisia 2026-07-02 tehdyn GitHub API -tarkistuksen perusteella.

julkinen hakemistonäkyvyystilannekuvalähde

Avaa organisaatio

GitHub-repositoriot ovat julkisen kooditilan lähde. Lisenssi, nykyiset tagit, julkinen näkyvyys ja julkaisusanamuoto tarkistettiin 2026-07-02 M10-T14-lopputarkistuksen yhteydessä.

Todistusekosysteemin rajaus

Selvennä roolit ennen todistustyökalujen vertailua.

Tämä on roolitaulukko, ei paremmuusjärjestys. Lean ja Rocq ovat edelleen todistusavustajien viite-ekosysteemejä; NPA esitetään sertifikaattikeskeisenä tutkimus- ja toteutustyönä.

Kohde	Lean	Rocq	NPA
Asema	Avoimen lähdekoodin ohjelmointikieli ja todistusavustaja.	Interaktiivinen teoreematodistin, jolla on pitkä tutkimushistoria.	Tutkimus- ja toteutusrepositorio sertifikaatit ensin -tarkistukseen.
Tyypillinen käyttö	Matematiikka, ohjelmistojen verifiointi ja ohjelmointi.	Matematiikka, määrittelyt, ohjelmien verifiointi ja ekstraktio.	Todistussertifikaattien, riippumattoman tarkistuksen ja pienen luotetun perustan tutkimus.
Näyttöraja	Sen oma luotettu ydin ja ekosysteemi määrittävät tarkistusrajan.	Sen oma ydin ja tarkistetut kehitykset määrittävät tarkistusrajan.	Kanoninen .npcert-artefakti siirtyy generoinnista tarkistukseen.
Miten tämä sivu käsittelee sitä	Viite oppimiseen, vertailuun ja yhteentoimivuuteen.	Viite oppimiseen, vertailuun ja formalisointimenetelmiin.	Finite Fieldin tutkimusprojekti, ei tuotelupaus.
Raja	Erikoisosaamista tarvitaan edelleen.	Erikoisosaamista tarvitaan edelleen.	NPA ei tällä hetkellä ole käytännön korvaaja Leanille tai Rocqille.

Leanin virallinen sivusto Rocq Proverin virallinen sivusto NPA GitHubissa

Lähteet

Julkaise lähdekartta tulkinnan rinnalla.

Lähteet näytetään, jotta lukija näkee, mitkä väitteet tulevat julkisista repositorioista, virallisilta todistustyökalujen sivustoilta ja yrityksen omasta kontekstista.

S01

finitefield-org/npa

Ensisijainen lähde NPA:n tarkoitukselle, luottamusmallille, v0.2.0:n nykyisen repositoriotagin sanamuodolle, komennoille, repositoriorakenteelle ja lisenssille.

Avaa lähde S02

Finite Fieldin GitHub-organisaatio

Ensisijainen lähde julkisten repositorioiden näkyvyydelle, uusimmille git-tageille, julkaisusivuille ja Lab-repositorioperheen tilannekuvalle, joka tarkistettiin 2026-07-02.

Avaa lähde S03

Leanin virallinen sivusto

Ensisijainen lähde Leanin julkiselle asemoinnille, tarkistettu 2026-07-02.

Avaa lähde S04

Leanin kieliviite

Ensisijainen lähde riippuvaisten tyyppien teorialle ja ytimen viitekontekstille, tarkistettu 2026-07-02.

Avaa lähde S05

Rocq Proverin virallinen sivusto

Ensisijainen lähde Rocqin julkiselle asemoinnille, tarkistettu 2026-07-02.

Avaa lähde S06

FINITE FIELD -yrityssivusto

Yrityslähde Finite Fieldin brändille ja liiketoimintakontekstille.

Avaa lähde

UKK

NPA:n tila ja verifioinnin rajat.

Vastaukset korostavat luottamusrajaa ennen kuin lukija sekoittaa tutkimussivun käyttöönotettuun todistusavustajapalveluun.

Lue yrityksestä

01 Onko tämä sivu tuotetakuu?

Ei. NPA esitetään tässä tutkimus- ja toteutusrepositoriona.

02 Voiko NPA korvata Leanin tai Rocqin?

Ei. NPA ei ole käytännön korvaaja Leanille tai Rocqille.

03 Ajaako sivu oikeaa NPA-verifiointia?

Ei. Selainpohjainen simulaatio ei aja NPA:ta, Rustia, WASMia tai oikeita todistussertifikaatteja.

04 Mikä lasketaan tässä näytöksi?

Sertifikaattiartefakti, deterministiset tiivisteet, Rust-ytimen/verifioijan tulos, lähteestä riippumattoman vertailutarkistimen tulos ja aksioomaraportti muodostavat tarkistuspuolen näytön.

05 Mitkä faktat on tarkistettava uudelleen?

Nykyinen julkinen versio, repositorioiden näkyvyys, työkaluketjun kiinnitykset, lisenssiteksti ja lähdesanamuodot tarkistettiin uudelleen 2026-07-02.

Todistuskurista operatiiviseen työhön

Käytä samaa näyttökuria, kun liiketoimintapäätökseen on voitava luottaa.

Liiketoimintajärjestelmissä hyödyllinen opetus ei ole teoreemojen todistamisen lisääminen kaikkialle. Olennaista on päättää, mitä on tuotettava, tarkistettava, lokitettava, korjattava ja hyväksyttävä ihmisten toimesta.

Tarkista liiketoimintaongelma Katso prototyyppi