Stato pubblico
Repository di ricerca e implementazione
Il repository GitHub è pubblico, ma questa pagina descrive un repository di ricerca e implementazione, non un servizio distribuito.
Torna a Math Lab
NPA / Controllo delle prove centrato sui certificati
NPA: esporre il confine delle evidenze prima di fidarsi di un risultato.
Questa pagina ricostruisce la sezione NPA di Math Lab come pagina autonoma di evidenze: stato pubblico, modello di fiducia, pipeline di prova, registro delle affermazioni, repository, fonti e formulazione esplicita di non sostituzione.
- Stato pubblico
- Repository di ricerca
- Presentato come ricerca e implementazione, non come servizio di garanzia in produzione.
- Ricontrollo pubblico
- 2026-07-02 / NPA v0.2.0
- Ultimi git tag verificati: npa v0.2.0, npa-std v0.1.0, npa-mathlib v0.1.30.
- Licenza
- Apache-2.0
- Apache-2.0 è stata verificata per npa, npa-std e npa-mathlib il 2026-07-02.
Ricontrollo pubblico: 2026-07-02. L’ultimo git tag del repository NPA è v0.2.0; npa-std è v0.1.0; npa-mathlib è v0.1.30. Le versioni fissate nei README sono mostrate come contesto specifico del repository e non sono accorpate in un’unica affermazione sulla versione di NPA.
Stato pubblico
Dichiara cosa è pubblico, cosa costituisce evidenza e quando è stato ricontrollato.
Questa pagina rende visibile la propria base: un’istantanea locale, una fonte pubblica in un repository e la data del ricontrollo finale prima del lancio.
Ricontrollo pubblico
2026-07-02
Il controllo delle fonti pubbliche è stato completato il 2026-07-02. La ricostruzione originale usa ancora l’istantanea locale del 2026-06-21.
Evidenza
Certificati e hash
L’istantanea della fonte registra canonical .npcert, certificate_hash, export_hash, axiom_report_hash e i verdetti dei verificatori.
Licenza
Apache-2.0 verificata
Apache-2.0 è stata verificata per npa, npa-std e npa-mathlib tramite metadati LICENSE pubblici il 2026-07-02.
Confine
NPA non è un sostituto pratico di Lean o Rocq. La simulazione di ispezione nel browser non esegue NPA. Tag pubblici, licenza e visibilità dei repository sono stati verificati il 2026-07-02 per il ricontrollo finale prima della pubblicazione.
Confine di fiducia
Fai attraversare il confine delle evidenze solo a un certificato canonico.
Il confine non riguarda quale strumento sembri sofisticato, ma quale artefatto possa diventare evidenza dopo una verifica indipendente.
Parser, elaboratore, tattiche, automazione, ricerca di teoremi, plugin, sistemi di IA, file sorgente, file di replay, indici di teoremi, piani di pubblicazione, stato CI, pagine delle release e metadati del registro restano sul lato non affidabile dei candidati.
Pipeline di prova / simulazione esplicativa
Mostra la pipeline esatta dai byte del certificato alle evidenze di verifica.
La simulazione nel browser non esegue NPA, Rust, WASM o veri certificati di prova. Visualizza l’ordine di verifica senza sorgente che gli artefatti reali devono soddisfare.
Percorso evidenziale CLI
npa package verify-certs --root . --checker reference --json
NPA / traccia di audit
PRONTO
- 01 Formato del certificatobyte canonici .npcert / certificato analizzabile / controllo del formato ATTESA
- 02 Hash del certificatobyte del certificato / certificate_hash / digest deterministico ATTESA
- 03 Verdetto del kernelcertificato / accettazione o rifiuto / report del verificatore Rust ATTESA
- 04 Verificatore di riferimentocertificato vincolato da hash / accettazione o rifiuto indipendente / report del verificatore senza sorgente ATTESA
- 05 Report sugli assiomipacchetto controllato / axiom_report_hash / inventario delle assunzioni ATTESA
Verdetto
La pipeline esplicativa non è ancora stata eseguita.Avvia la spiegazione per segnare in ordine il percorso di verifica senza sorgente.
Registro delle affermazioni
Separare le evidenze, i fatti sensibili al tempo e le affermazioni di confine.
La pagina non dipende da testi di ricerca approssimativi. Ogni dichiarazione pubblica è collegata a uno snapshot locale di riferimento, a una fonte e a un'azione per la pubblicazione.
| Affermazione | Formulazione pubblica | Stato | Fonte | Azione per la pubblicazione |
|---|---|---|---|---|
| CL-001 | NPA mette il certificato al centro: il confine verificabile è costituito dall'artefatto canonico .npcert e dal percorso di controllo che lo circonda. | Affermazione pubblica verificata | S01 / 2026-07-02 | Riesaminare quando cambia il README. |
| CL-002 | Il controllo pubblico del 02/07/2026 ha rilevato che il tag Git più recente del repository NPA era v0.2.0. I README dei pacchetti correlati mostrano ancora riferimenti specifici per repository, quindi la formulazione delle versioni resta limitata al singolo repository. | Ricontrollo pubblico verificato | S01 / S02 / 2026-07-02 | Mantenere la formulazione del tag limitata al singolo repository. |
| CL-003 | Lo snapshot locale di riferimento registra un vincolo alla toolchain Rust 1.95.0; non viene usato come affermazione di marketing. | Verificato, sensibile al tempo | S01 / 2026-07-02 | Ricontrollare se viene mostrata la versione della toolchain. |
| CL-004 | NPA non è un sostituto pratico di Lean o Rocq. Questo confine deve rimanere visibile accanto a qualsiasi confronto. | Affermazione di confine verificata | S01 / S03 / S05 / 2026-07-02 | Mantenere l'avvertenza. |
| CL-005 | npa-std e npa-mathlib sono repository pubblici distinti di pacchetti di teoremi nell'organizzazione finitefield-org. | Affermazione pubblica verificata | S01 / S02 / 2026-07-02 | Ricontrollare la visibilità dei repository se la pubblicazione viene rinviata o se i repository cambiano. |
| CL-006 | I repository npa, npa-std e npa-mathlib espongono ciascuno la licenza Apache-2.0 tramite i rispettivi metadati LICENSE pubblici. | Affermazione pubblica verificata | S01 / S02 / 2026-07-02 | Ricontrollare LICENSE in occasione di una versione principale. |
Repository e licenza
Rendi espliciti codice, repository dei pacchetti e visibilità dell’organizzazione.
I collegamenti ai repository puntano a fonti pubbliche, ma non garantiscono che questa pagina sia sincronizzata con l’ultimo stato di GitHub.
4 repository visualizzati
finitefield-org
npa
Toolchain di assistenza e verifica delle prove centrata sui certificati.
- Licenza
- Apache-2.0 verificata da LICENSE il 2026-07-02.
- Verifica
- Ultimo git tag: v0.2.0. Non è pubblicata una release GitHub più recente. Riferimento corrente alla toolchain nel README: NPA_GIT_TAG=v0.2.0.
sperimentaleRust / OCamlcertificato al centro
Apri repository
finitefield-org
npa-std
Repository del pacchetto standard di teoremi per le sorgenti di prova NPA.
- Licenza
- Apache-2.0 verificata da LICENSE il 2026-07-02.
- Verifica
- Ultimo git tag e release GitHub: v0.1.0. Versione dei metadati del pacchetto nel README: 0.1.0; versione fissata della toolchain: NPA_GIT_TAG=v0.1.1.
sperimentalepacchetto di teoremisorgente di prova
Apri repository
finitefield-org
npa-mathlib
Repository di ricerca per una libreria di matematica formale.
- Licenza
- Apache-2.0 verificata da LICENSE il 2026-07-02.
- Verifica
- Ultimo git tag: v0.1.30. Ultima release GitHub: v0.1.9. Versione dei metadati del pacchetto nel README: 0.2.1; versione fissata della toolchain: NPA_GIT_TAG=v0.1.1.
ricercamatematica formalelibreria
Apri repository
finitefield-org
Organizzazione GitHub di Finite Field
Istantanea pubblica dell’organizzazione per la famiglia di repository Lab.
- Licenza
- Si applicano licenze specifiche per repository
- Verifica
- npa, npa-std e npa-mathlib sono pubblici secondo il ricontrollo dell’API GitHub del 2026-07-02.
indice pubblicosnapshot di visibilitàfonte
Apri organizzazione
Nessun repository corrisponde alla ricerca corrente.
I repository GitHub sono la fonte dello stato pubblico del codice. Licenza, tag correnti, visibilità pubblica e formulazione delle release sono stati verificati il 2026-07-02 nel ricontrollo finale M10-T14.
Protezione dell'ecosistema delle prove
Chiarire i ruoli prima di confrontare gli strumenti di prova.
Questa è una tabella dei ruoli, non una classifica. Lean e Rocq restano gli ecosistemi di riferimento per gli assistenti alla dimostrazione; NPA è presentato come lavoro di ricerca e implementazione incentrato sui certificati.
| Elemento | Lean | Rocq | NPA |
|---|---|---|---|
| Posizione | Linguaggio di programmazione open source e assistente alla dimostrazione. | Dimostratore interattivo di teoremi con una lunga storia di ricerca. | Repository di ricerca e implementazione per il controllo incentrato sui certificati. |
| Uso tipico | Matematica, verifica del software e programmazione. | Matematica, specifiche, verifica dei programmi ed estrazione. | Ricerca su certificati di dimostrazione, controllo indipendente e una base fidata ridotta. |
| Confine dell'evidenza | Il proprio kernel fidato e l'ecosistema definiscono il confine di controllo. | Il proprio kernel e gli sviluppi controllati definiscono il confine di controllo. | L'artefatto canonico .npcert passa dalla generazione al controllo. |
| Come viene considerato in questa pagina | Riferimento per apprendimento, confronto e interoperabilità. | Riferimento per apprendimento, confronto e metodi di formalizzazione. | Progetto di ricerca di Finite Field, non una promessa di prodotto. |
| Confine | Sono ancora necessarie conoscenze specialistiche. | Sono ancora necessarie conoscenze specialistiche. | Attualmente NPA non è un sostituto pratico di Lean o Rocq. |
Fonti
Pubblica la mappa delle fonti insieme all’interpretazione.
Le fonti consentono al lettore di distinguere le affermazioni provenienti da repository pubblici, siti ufficiali degli strumenti di prova e contesto aziendale.
S01
finitefield-org/npa
Fonte primaria per scopo e modello di fiducia di NPA, formulazione del tag corrente v0.2.0, comandi, struttura del repository e licenza.
Apri fonte S02Organizzazione GitHub di Finite Field
Fonte primaria per visibilità pubblica dei repository, ultimi git tag, pagine delle release e istantanea della famiglia Lab verificata il 2026-07-02.
Apri fonte S03Sito ufficiale Lean
Fonte primaria per il posizionamento pubblico di Lean, verificata il 2026-07-02.
Apri fonte S04Riferimento del linguaggio Lean
Fonte primaria per la teoria dei tipi dipendenti e il contesto di riferimento del kernel, verificata il 2026-07-02.
Apri fonte S05Sito ufficiale Rocq Prover
Fonte primaria per il posizionamento pubblico di Rocq, verificata il 2026-07-02.
Apri fonte S06Sito aziendale FINITE FIELD
Fonte aziendale per il marchio Finite Field e il contesto commerciale.
Apri fonteFAQ
Stato di NPA e confini della verifica.
Le risposte evidenziano il confine di fiducia prima che una pagina di ricerca venga confusa con un servizio di assistenza alla prova distribuito.
Scopri l’azienda01 Questa pagina costituisce una garanzia di prodotto?
No. NPA è presentato qui come repository di ricerca e implementazione.
02 NPA può sostituire Lean o Rocq?
No. NPA non è un sostituto pratico di Lean o Rocq.
03 La pagina esegue una vera verifica NPA?
No. La simulazione nel browser non esegue NPA, Rust, WASM o veri certificati di prova.
04 Che cosa conta come evidenza qui?
L’artefatto del certificato, gli hash deterministici, il risultato del Rust kernel/verifier, quello del verificatore di riferimento senza sorgente e il rapporto sugli assiomi costituiscono le evidenze dal lato della verifica.
05 Quali fatti devono essere ricontrollati?
Versione pubblica attuale, visibilità dei repository, versioni fissate della toolchain, testo della licenza e formulazione delle fonti sono stati ricontrollati il 2026-07-02.
Dalla disciplina della prova alle operazioni
Applica la stessa disciplina delle evidenze quando una decisione aziendale deve essere affidabile.
Per i sistemi aziendali, la lezione utile non è aggiungere ovunque la dimostrazione di teoremi. È decidere cosa deve essere generato, verificato, registrato, corretto e approvato dalle persone.