NPA / Certifikatbaseret beviskontrol

NPA: Vis grænsen for bevisevidens, før et resultat betros.

Denne side genskaber NPA-afsnittet fra Math Lab som en selvstændig evidensside: offentlig status, tillidsmodel, bevispipeline, påstandsregister, repositorier, kilder og tydelig tekst om, at NPA ikke er en erstatning.

Undersøg tillidsgrænsen Åbn GitHub-repository

Offentlig status: Forskningsrepository; Vises som forskning og implementering, ikke som en produktionssikringstjeneste.
Offentlig genkontrol: 2026-07-02 / NPA v0.2.0; Seneste kontrollerede git-tags: npa v0.2.0, npa-std v0.1.0, npa-mathlib v0.1.30.
Licens: Apache-2.0; Apache-2.0 blev verificeret for npa, npa-std og npa-mathlib den 02.07.2026.

Offentlig genkontrol: 02.07.2026. Det seneste git-tag i NPA-repositoriet er v0.2.0; npa-std er v0.1.0; npa-mathlib er v0.1.30. Pakkernes README-bindinger vises som repositoryspecifik kontekst og sammenlægges ikke til én NPA-versionspåstand.

Forhåndsvisning af NPA-evidenssiden med certifikatkontrol og undersøgelse af tillidsgrænsen — Grafikken er en statisk forhåndsvisning af resultatet af certifikatkontrollen og forklaringen af tillidsgrænsen. Den er ikke et aktivt NPA-spor.

Offentlig status

Angiv, hvad der er offentligt, hvad der er evidens, og hvornår det blev genkontrolleret.

Siden synliggør sit grundlag: et lokalt sandhedssnapshot, en offentlig repositorykilde og datoen for den endelige kontrol før lancering.

Offentlig status

Forsknings- og implementeringsrepository

GitHub-repositoriet er offentligt, men denne side beskriver et forsknings- og implementeringsrepository, ikke en implementeret tjeneste.

Offentlig genkontrol

2026-07-02

Genkontrollen af offentlige kilder blev afsluttet den 02.07.2026. Den oprindelige kilderekonstruktion bruger stadig det lokale sandhedssnapshot fra 21.06.2026.

Evidens

Certifikater og hashes

Kildesnapshottet registrerer kanonisk .npcert, certificate_hash, export_hash, axiom_report_hash og kontrolafgørelser.

Licens

Apache-2.0 verificeret

Apache-2.0 blev verificeret for npa, npa-std og npa-mathlib via offentlige LICENSE-metadata den 02.07.2026.

Grænse

NPA er ikke en praktisk erstatning for Lean eller Rocq. Den distribuerede browserkontrolsimulering kører ikke NPA selv. Offentlige tags, licens og repositorysynlighed blev kontrolleret den 02.07.2026 til den endelige offentliggørelsesgenkontrol.

Tillidsgrænse

Flyt kun et kanonisk certifikat over evidensgrænsen.

Grænsen handler ikke om, hvilket værktøj der ser avanceret ud. Den handler om, hvilken artefakt der må blive evidens efter uafhængig kontrol.

Parser, elaborator, taktikker, automatisering, teoremsøgning, plugins, AI-systemer, kildefiler, replayfiler, teoremindekser, offentliggørelsesplaner, CI-status, udgivelsessider og registermetadata forbliver på den ikke-betroede kandidatside.

Bevispipeline / forklarende simulering

Vis det præcise forløb fra certifikatbytes til kontrolevidens.

Browsersimuleringen kører hverken NPA selv, Rust, WASM eller virkelige beviscertifikater. Den visualiserer den kildefrie kontrolrækkefølge, som virkelige artefakter skal opfylde.

CLI-evidenssti

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

NPA / revisionsspor KLAR

01 Certifikatformatkanoniske .npcert-bytes / parsbar certifikat / formatkontrol VENT
02 Certifikat-hashcertifikatbytes / certificate_hash / deterministisk digest VENT
03 Kerneafgørelsecertifikat / accept eller afvisning / Rust-verifikatorrapport VENT
04 Referencekontrolhashbundet certifikat / uafhængig accept eller afvisning / kildefri kontrolrapport VENT
05 Aksiomrapportkontrolleret pakke / axiom_report_hash / antagelsesoversigt VENT

Afgørelse

Det forklarende forløb er endnu ikke kørt.

Kør forklaringen for at markere den kildefrie kontrolsti i rækkefølge.

Påstandsregister

Adskil evidens, tidsfølsomme fakta og grænsepåstande.

Siden afhænger ikke af løs forskningstekst. Hver offentlig udtalelse er knyttet til et lokalt sandhedssnapshot, en kilde og en handling før offentliggørelse.

Påstand	Offentlig formulering	Status	Kilde	Handling før offentliggørelse
CL-001	NPA sætter certifikatet først: Den reviderbare grænse er den kanoniske .npcert-artefakt og kontrolforløbet omkring den.	Verificeret offentlig påstand	S01 / 2026-07-02	Gennemgå igen, når README ændres.
CL-002	Den offentlige genkontrol den 02.07.2026 fandt, at det seneste git-tag i NPA-repositoriet var v0.2.0. README-filerne for de tilknyttede pakker viser fortsat repositoryspecifikke bindinger, så versionsformuleringen forbliver afgrænset til det enkelte repository.	Verificeret offentlig genkontrol	S01 / S02 / 2026-07-02	Hold tag-formuleringen afgrænset til det enkelte repository.
CL-003	Det lokale sandhedssnapshot registrerer en binding til Rust 1.95.0-værktøjskæden; den bruges ikke som en markedsføringspåstand.	Verificeret, tidsfølsom	S01 / 2026-07-02	Kontrollér igen, hvis værktøjskædens version vises.
CL-004	NPA er ikke en praktisk erstatning for Lean eller Rocq. Denne grænse skal være synlig ved enhver sammenligning.	Verificeret grænsepåstand	S01 / S03 / S05 / 2026-07-02	Bevar ansvarsfraskrivelsen.
CL-005	npa-std og npa-mathlib er separate offentlige repositorier for teorempakker i organisationen finitefield-org.	Verificeret offentlig påstand	S01 / S02 / 2026-07-02	Kontrollér repositoriernes synlighed igen, hvis offentliggørelsen forsinkes, eller repositorierne ændres.
CL-006	Repositorierne npa, npa-std og npa-mathlib viser hver især Apache-2.0-licensen via deres offentlige LICENSE-metadata.	Verificeret offentlig påstand	S01 / S02 / 2026-07-02	Kontrollér LICENSE igen ved en større udgivelse.

Repositorier og licens

Gør kode, pakkerepositorier og organisationssynlighed tydelige.

Repositorylinks er henvisninger til offentlige kilder, ikke garantier for, at denne side er synkroniseret med den seneste GitHub-status.

4 repositorier vist

finitefield-org

npa

Certifikatbaseret bevisassistance og verifikationsværktøjskæde.

Licens: Apache-2.0 verificeret fra LICENSE den 02.07.2026.
Verifikation: Seneste git-tag: v0.2.0. Der er ikke offentliggjort en seneste GitHub-udgivelse. README's aktuelle værktøjskædereference: NPA_GIT_TAG=v0.2.0.

eksperimenteltRust / OCamlcertifikatbaseret

Åbn repository

finitefield-org

npa-std

Repository for standardteorempakken til NPA-beviskilder.

Licens: Apache-2.0 verificeret fra LICENSE den 02.07.2026.
Verifikation: Seneste git-tag og GitHub-udgivelse: v0.1.0. Version i README-pakkemetadata: 0.1.0; pakkens værktøjskædebinding: NPA_GIT_TAG=v0.1.1.

eksperimenteltteorempakkebeviskilde

Åbn repository

finitefield-org

npa-mathlib

Forskningsrepository for et bibliotek med formel matematik.

Licens: Apache-2.0 verificeret fra LICENSE den 02.07.2026.
Verifikation: Seneste git-tag: v0.1.30. Seneste GitHub-udgivelse: v0.1.9. Version i README-pakkemetadata: 0.2.1; pakkens værktøjskædebinding: NPA_GIT_TAG=v0.1.1.

forskningformel matematikbibliotek

Åbn repository

finitefield-org

Finite Field GitHub-organisation

Offentligt snapshot af organisationen for Lab-repositoryfamilien.

Licens: Repositoryspecifikke licenser gælder
Verifikation: npa, npa-std og npa-mathlib er offentlige ifølge GitHub API-genkontrollen den 02.07.2026.

offentligt indekssynlighedssnapshotkilde

Åbn organisation

GitHub-repositorierne er kilden til offentlig kodestatus. Licens, aktuelle tags, offentlig synlighed og udgivelsesformulering blev kontrolleret den 02.07.2026 som den endelige M10-T14-genkontrol.

Værn for bevisøkosystemet

Afklar rollerne, før bevisværktøjer sammenlignes.

Dette er en rolletabel, ikke en rangliste. Lean og Rocq er fortsat referenceøkosystemer for bevisassistenter; NPA præsenteres som certifikatcentreret forsknings- og implementeringsarbejde.

Emne	Lean	Rocq	NPA
Position	Programmeringssprog med åben kildekode og bevisassistent.	Interaktiv teorembeviser med en lang forskningshistorie.	Forsknings- og implementeringsrepository til certifikatbaseret kontrol.
Typisk anvendelse	Matematik, softwareverifikation og programmering.	Matematik, specifikationer, programverifikation og ekstraktion.	Forskning i beviscertifikater, uafhængig kontrol og en lille betroet base.
Evidensgrænse	Dets egen betroede kerne og økosystem definerer kontrolgrænsen.	Dets egen kerne og kontrollerede udviklinger definerer kontrolgrænsen.	Den kanoniske .npcert-artefakt går fra generering til kontrol.
Sådan behandles det på siden	Reference til læring, sammenligning og interoperabilitet.	Reference til læring, sammenligning og formaliseringsmetoder.	Finite Field-forskningsprojekt, ikke et produktløfte.
Grænse	Specialistviden er stadig nødvendig.	Specialistviden er stadig nødvendig.	NPA er på nuværende tidspunkt ikke en praktisk erstatning for Lean eller Rocq.

Leans officielle websted Rocq Provers officielle websted NPA på GitHub

Kilder

Vis kildekortet sammen med fortolkningen.

Kilderne vises, så læseren kan se, hvilke påstande der kommer fra offentlige repositorier, officielle websteder for bevisværktøjer og virksomhedskontekst.

S01

finitefield-org/npa

Primær kilde til NPA's formål, tillidsmodel, formulering af det aktuelle repositorytag v0.2.0, kommandoer, repositorystruktur og licens.

Åbn kilde S02

Finite Field GitHub-organisation

Primær kilde til offentlig repositorysynlighed, seneste git-tags, udgivelsessider og snapshottet af Lab-repositoryfamilien kontrolleret den 02.07.2026.

Åbn kilde S03

Leans officielle websted

Primær kilde til Leans offentlige positionering, kontrolleret den 02.07.2026.

Åbn kilde S04

Lean-sprogreference

Primær kilde til kontekst om afhængig typeteori og kernereference, kontrolleret den 02.07.2026.

Åbn kilde S05

Rocq Provers officielle websted

Primær kilde til Rocqs offentlige positionering, kontrolleret den 02.07.2026.

Åbn kilde S06

FINITE FIELD-virksomhedswebsted

Virksomhedskilde til Finite Field-brandet og forretningskonteksten.

Åbn kilde

FAQ

NPA-status og verifikationsgrænser.

Svarene fremhæver tillidsgrænsen, før læsere forveksler en forskningsside med en implementeret bevisassistenttjeneste.

Læs om virksomheden

01 Er denne side en produktgaranti?

Nej. NPA vises her som et forsknings- og implementeringsrepository.

02 Kan NPA erstatte Lean eller Rocq?

Nej. NPA er ikke en praktisk erstatning for Lean eller Rocq.

03 Kører siden en virkelig NPA-verifikation?

Nej. Browsersimuleringen kører hverken NPA selv, Rust, WASM eller virkelige beviscertifikater.

04 Hvad tæller som evidens her?

Certifikat-artefakten, deterministiske hashes, resultatet fra Rust-kernen/verifikatoren, resultatet fra den kildefrie referencekontrol og aksiomrapporten udgør evidensen på kontrolsiden.

05 Hvilke fakta kræver genkontrol?

Aktuel offentlig version, repositorysynlighed, værktøjskædebindinger, licenstekst og kildeformulering blev genkontrolleret den 02.07.2026.

Fra bevisdisciplin til drift

Brug samme evidensdisciplin, når en forretningsbeslutning skal være troværdig.

For forretningssystemer er den nyttige lære ikke at tilføje teorembevis overalt. Det handler om at beslutte, hvad der skal genereres, kontrolleres, logges, rettes og godkendes af mennesker.

Kontrollér forretningsproblemet Se prototypen