01 / Riba
Patikimą bazę laikyti mažą
Sudėtingų generatorių ar DI nestatykite pasitikėjimo centre. Aiškiai parodykite mažą tikrinimo pusę.
Finite Field / Math Lab
Kurkite teisingumo įrodymus, o ne tik greitus rezultatus.
Math Lab rodo, kaip tvarkome matematinį modeliavimą, teoremų įrodymą, formalųjį tikrinimą, atkuriamumą ir patikimą įgyvendinimą, neperdėdami įrodymų galios.
- Vieši projektai
- NPA / STD / MATHLIB
- Pagrindinė kalba
- Rust
- NPA momentinė kopija
- v0.1.1
Įrodymų auditas / koncepcinis vaizdas
Tik skaitymui
01 kanoniniai baitai / formatas GERAI
02 certificate_hash GERAI
03 priklausomo įrodymo tikrinimas GERAI
04 verdiktas be šaltinio GERAI
Pasitikėjimo riba matoma
Šis puslapis neteigia, kad NPA yra praktinis Lean ar Rocq pakaitalas, o naršyklės simuliacija nevykdo NPA.
Laboratorijos principas
Publikuokite ne tik rezultatus, bet ir tikrinimo ribą.
Išvada „veikė“, „buvo greita“ arba „įrodyta“ nepakankama. Atskirai rodome įvestis, prielaidas, patikimas dalis, nepriklausomai tikrinamus artefaktus ir neišspręstus klausimus.
02 / Įrodymai
Įrodymus paversti artefaktais
Sertifikatus, maišas, prielaidų sąrašus, testavimo sąlygas ir žurnalus palikite tokia forma, kurią kiti gali patikrinti.
03 / Atkartojimas
Projektuoti atkuriamumui
Užfiksuokite įrankių grandines, įvesties duomenis, vykdymo komandas ir kriterijus, kad rezultatą būtų galima patikrinti dar kartą.
04 / Sąžiningumas
Neperdėti tyrimo būsenos
Praktinius metodus, eksperimentus ir tyrimus rodykite atskirai. Ribojimus pateikite šalia rezultatų.
METODO PERŽIŪRA
Paslaugos metodo kategorija, kuriai prieš vadinant parengta projektui dar reikia apimties, atsakomybės, kliento įrodymų ir patvirtinimo.
EKSPERIMENTINIS
Veikiantis įgyvendinimas yra, bet mastelis, suderinamumas, našumas ar specifikacijos dar gali keistis. Būtina nurodyti versiją ir atkūrimo veiksmus.
TYRIMAS
Projektavimas, vertinimas, įrodymas arba įgyvendinimas dar vyksta. Tai nereiškia komercinio prieinamumo ar užbaigtumo.
Tyrimų portfelis
Tyrimus peržiūrėkite pagal brandą ir artefaktus.
Kiekviena kortelė rodo brandą, artefaktus, dabartinę būseną ir kitą validaciją. Paieška ir filtrai naudoja tik naršyklės būseną.
8 sritys
EKSPERIMENTINIS
ATVIRASIS KODAS
01
Nano Proof Auditor
Nuo sertifikato pradedama įrodymų įrankių grandinė
Tyrimo įrankių grandinė, kuri kanoninius įrodymo sertifikatus ir mažą tikrinimo bazę laiko priklausomų įrodymų peržiūros centru.
- Artefaktai
- šaltinis / specifikacija / CI šablonai
- Dabartinė būsena
- v0.1.1 vieša momentinė kopija
- Kita validacija
- išoriniai teoremų paketai ir nepriklausoma patikra
EKSPERIMENTINIS
ATVIRASIS KODAS
02
NPA standartinė biblioteka
Logika / Nat / List / Algebra
Standartinių teoremų paketų repozitorija pakartotinai naudojamiems NPA pagrindams.
- Artefaktai
- šaltinis / įrodymų paketai
- Dabartinė būsena
- vieša padalinta repozitorija
- Kita validacija
- paketo apimtis ir suderinamumas
TYRIMAS
ATVIRASIS KODAS
03
NPA matematikos biblioteka
Formaliosios matematikos biblioteka
Bibliotekos kryptis, skirta matematines teoremas saugoti kaip nepriklausomai tikrinamus įrodymų paketus.
- Artefaktai
- šaltinis / įrodymų paketai
- Dabartinė būsena
- kuriama vieša repozitorija
- Kita validacija
- bibliotekos struktūra ir priklausomybių auditas
METODO PERŽIŪRA
METODAS
04
Apriboto planavimo modeliai
Grafikai / maršrutai / priskyrimai
Metodas, skirtas griežtiems apribojimams ir vertinimo metrikoms atskirti pamainų, vizitų, maršrutų, gamybos ir priskyrimo darbuose.
- Artefaktai
- modelis / prototipas / paaiškinimo ataskaita
- Dabartinė būsena
- paslaugos metodas; viešas teiginys ribojamas metodo peržiūra
- Kita validacija
- kliento įrodymai ir apimties patvirtinimas
TYRIMAS
MATAVIMAS
05
Atkuriamas sprendiklių vertinimas
Etalonai ir įrodymai
Programa, skirta prieš našumo teiginius užfiksuoti egzempliorių rinkinius, aparatinę įrangą, laiko ribas, atsitiktines sėklas ir neapdorotus žurnalus.
- Artefaktai
- etalonų registras / neapdoroti žurnalai / ataskaita
- Dabartinė būsena
- tyrimų programos projektas
- Kita validacija
- pirmasis viešas etalonų korpusas
TYRIMAS
FORMALIEJI METODAI
06
Kritinės verslo logikos tikrinimas
Verslo sistemų invariantai
Tyrimas, kaip mokesčius, leidimus, atsargas ir būsenos perėjimus atskirti į specifikacijas ir invariantus.
- Artefaktai
- specifikacija / invariantai / testo arba įrodymo ataskaita
- Dabartinė būsena
- apimties tyrimas
- Kita validacija
- pasirinkti vieną ribotą, gamybai artimą atvejį
EKSPERIMENTINIS
INŽINERIJA
07
Maži patikimi komponentai Rust kalba
Maži pasitikėjimui svarbūs komponentai
Įgyvendinimo darbas, kuriame pasitikėjimui svarbios dalys, pavyzdžiui, tikrintuvai ir maišos, laikomos pakankamai mažos peržiūrai.
- Artefaktai
- NPA branduolys / sertifikato crate / etaloninis tikrintuvas
- Dabartinė būsena
- viešas įgyvendinimas NPA
- Kita validacija
- nepriklausomo tikrintuvo suderinamumas
TYRIMAS
DI × ĮRODYMAS
08
DI pagalba ir nepriklausoma patikra
Generuokite laisvai, tikrinkite griežtai
Tyrimų kryptis, kurioje DI naudojamas kandidatams generuoti, o galutinis įrodymas tikrinamas nepriklausomai.
- Artefaktai
- kandidatų generatorius / sertifikatas / tikrintuvo ataskaita
- Dabartinė būsena
- tyrimų kryptis, suderinama su NPA pasitikėjimo modeliu
- Kita validacija
- išmatuota autorystės eiga
Atitinkančios tyrimų srities nerasta.
Pabandykite kitą raktažodį arba grąžinkite brandos filtrą į visas reikšmes.
Nano Proof Auditor
Atskirkite įrodymų generavimą nuo to, kuo pasitikime.
NPA yra nuo sertifikato pradedama įrankių grandinė priklausomiems įrodymams. Sąsajos, taktikos, teoremų paieška, įskiepiai, DI, šaltinio failai ir CI būsena gali padėti kurti kandidatus, bet nėra patikimas įrodymo pagrindas.
EKSPERIMENTINISATVIRASIS KODASAPACHE-2.0
Dabartinė momentinė kopija
v0.1.1
Vieša informacija patikrinta 2026-06-21.
Pirminis branduolys
Rust
Rust tikrintuvas ir branduolys priklauso tikrinimo pusei.
Audito artefaktas
.npcert
Kanoniniai sertifikato baitai yra tikrinamas objektas.
Pakartotinio tikrinimo taškas
rankinė peržiūra
Prieš publikavimą reikia peržiūrėti repozitorijos būseną ir paketų matomumą.
Pasitikėjimo ribos tyriklis
Peržiūrėkite, kuo pasitikima ir kuo ne.
Spustelėkite kiekvieną mazgą, kad pamatytumėte, ką jis daro, ką sukuria ir kokios patikros dar reikia.
NEPATIKIMA
PATIKRINTA
Svarbi riba
Šiuo metu NPA nėra praktinis Lean ar Rocq pakaitalas. Šis puslapis aiškina sertifikatais grindžiamą tyrimo projektavimą ir negarantuoja komercinių sistemų be klaidų ar automatinio teoremų sprendimo.
Sertifikato patikra / paaiškinamoji simuliacija
Pajuskite sertifikato tikrinimo eigą.
Naršyklės sąveika paaiškina tikrinimo eigą. Ji nevykdo NPA, Rust, WASM ar tikrų įrodymo sertifikatų.
CLI pavyzdys
npa package verify-certs --root . --checker reference --json
NPA / audito pėdsakas
PARENGTA
- 01 Perskaityti sertifikatąkanoniniai baitai / formatas LAUKIA
- 02 Patikrinti sertifikato maišącertificate_hash LAUKIA
- 03 Patikrinti branduoliupriklausomo įrodymo tikrinimas LAUKIA
- 04 Pakartoti etaloniniu tikrintuvuverdiktas be šaltinio LAUKIA
- 05 Palyginti aksiomų ataskaitąaksiomų ataskaitos maiša LAUKIA
Verdiktas
Paaiškinimas dar nepaleistas.Paleiskite paaiškinimą, kad pamatytumėte veiksmus iš eilės.
Įrodymų ekosistema
Aiškinkite vaidmenis, o ne rikiuokite įrankius.
Lean ir Rocq yra brandžios įrodymų asistentų ekosistemos. NPA čia pateikiamas kaip sertifikatų centre esantis tyrimo ir įgyvendinimo projektas, o ne kaip pakaitalų reitingas.
| Elementas | Lean | Rocq | NPA |
|---|---|---|---|
| Pozicija | Atvirojo kodo programavimo kalba ir įrodymų asistentas. | Interaktyvus teoremų įrodiklis su ilga tyrimų istorija. | Tyrimo ir įgyvendinimo repozitorija, skirta nuo sertifikatų pradedamam tikrinimui. |
| Tipinis naudojimas | Matematika, programinės įrangos tikrinimas ir programavimas. | Matematika, specifikacijos, programų tikrinimas ir išgavimas. | Tyrimai apie įrodymo sertifikatus ir nepriklausomą tikrinimą. |
| Akcentas | Išplečiamumas, bibliotekos ir interaktyvus įrodinėjimas. | Išraiškingumas, brandūs metodai ir bibliotekos. | Maža patikima bazė ir kanoniniai sertifikatai. |
| Kaip šis puslapis tai vertina | Mokymosi, palyginimo ir sąveikumo atskaita. | Mokymosi, palyginimo ir formalizavimo metodų atskaita. | Finite Field tyrimų projektas. |
| Riba | Vis dar reikia specialisto žinių. | Vis dar reikia specialisto žinių. | Šiuo metu nelaikomas praktiniu Lean ar Rocq pakaitalu. |
Tyrimo metodas
„Veikė“ paverskite pakartojama tikrinimo procedūra.
Rezultatas tampa stipresnis, kai kas nors gali jį pakartoti, patikrinti ir atmesti tomis pačiomis sąlygomis.
Klausimas
Apibrėžkite, ką reikia tikrinti: našumą, teisingumą, suderinamumą ar apimtį.
Prielaidos
Prieš vertinimą užrašykite prielaidas, išimtis, aksiomas, duomenų spragas ir šališkumą.
Artefaktas
Išsaugokite šaltinį, sertifikatus, įvestis, vykdymo žurnalus ir maišas.
Nepriklausoma patikra
Rezultatus tikrinkite keliu, kuris skiriasi nuo generavimo pusės.
Etaloninis vertinimas
Užfiksuokite aparatinę įrangą, versijas, laiko ribas, egzempliorių rinkinius ir atsitiktines sėklas.
Ribos
Publikuokite nesėkmes, nepalaikomus atvejus, našumo ribas ir kitą validaciją.
Atkuriamumo konstruktorius
Patikrinkite, ko tyrimo publikacijai dar trūksta.
Kontrolinis sąrašas apdorojamas tik naršyklėje. Tai nėra sertifikavimo balas.
Parengtis
0%Kitas veiksmas
Pirmiausia apibrėžkite tyrimo klausimą ir sėkmės sąlygą.Prieš pasirinkdami artefaktų formatus užfiksuokite, kas bus lyginama arba tikrinama.
Vieši artefaktai
Viešus artefaktus sekite iš vieno įėjimo taško.
Puslapis vengia GitHub API kvietimų vykdymo metu. Repozitorijos būsena yra peržiūrėta momentinė kopija, kurią prieš publikavimą reikia patikrinti.
4 artefaktų
finitefield-org
npa
nuo sertifikato pradedama įrodymų įrankių grandinė
TIKRINIMAS
package verify-certs
finitefield-org
npa-std
standartinis teoremų paketas
VAIDMUO
Std.Logic / Nat / List
finitefield-org
npa-mathlib
formaliosios matematikos biblioteka
VAIDMUO
formalieji teoremų paketai
GitHub
finitefield-org
viešų repozitorijų indeksas
INDEKSAS
visos viešos repozitorijos
Paiešką atitinkančių viešų artefaktų nėra.
Publikavimo politika
Viešos repozitorijos, tyrimų pastabos ir etalonai turi turėti patikrinimo datą, brandą, atkūrimo veiksmus ir žinomus ribojimus. Žvaigždučių ir commit skaičiai nerodomi kaip tyrimo kokybės signalai.
Nuo laboratorijos prie operacijų
Tyrimų discipliną perkelkite į verslo sistemų projektavimą.
Ne kiekvienai kliento sistemai reikia teoremų įrodymo. Naudingiausia perkelti sprendimą, kuo reikia pasitikėti, ką lyginti, tikrinti, taisyti ir tvirtinti žmonėms.
Laboratorijos praktika
Atskirkite generavimą, skaičiavimą ir galutinę patikrą, o ne vienodai pasitikėkite kiekvienu sluoksniu.
Įvestis, išvestis, sertifikatus, maišas ir žurnalus laikykite peržiūrimais artefaktais.
Prieš lygindami rezultatus užfiksuokite duomenis, versijas, komandas ir vertinimo kriterijus.
Apribojimus, nesėkmingus atvejus ir neišspręstus klausimus publikuokite tokiu pat svoriu kaip rezultatus.
Kliento sistema
Apibrėžkite, kas įveda, kas peržiūri, kas keičia ir kas patvirtina rezultatą.
Rodykite apribojimus, vertinimo balus, atmestus kandidatus ir neišspręstus klausimus.
Išsaugokite sąlygų pakeitimus, skaičiavimo paleidimus ir galutinio patvirtinimo istoriją.
Automatinę išvestį padarykite koreguojamą, atmetamą ir paaiškinamą operatoriams.
01
Pamainos ir personalas
Taisyklių pažeidimus ir pageidavimų tenkinimą rodykite atskirai.
02 Transporto maršrutaiMaršruto priežastis, talpą, laiko langus ir išimtis palikite matomus.
03 Gamybos planavimasPaaiškinkite nesuplanuotą darbą, kliūtis ir paruošimo kompromisus.
04 Priskyrimas ir derinimasPrieš patvirtinimą parodykite kandidatų priežastis ir alternatyvas.
Tyrimų pastabos
Atnaujinimų istoriją ir įrodymus palikite skaitomus.
Ne kiekviena kortelė yra paskelbtas straipsnis. Rengiamos pastabos nelaikomos publikuotu darbu, kol neturi datų, šaltinių ir atkūrimo veiksmų.
NPA / dabartinė būsena
Kodėl sertifikatus verta laikyti centre
Kodėl galutinis įrodymas turėtų būti standartizuotas sertifikatas, tikrinamas mažu nepriklausomu keliu.
Peržiūrėti viešą repozitorijąProjektavimo pastaba / planuojama
Kaip paaiškinti optimizavimo rezultatus
Projektavimo pastaba apie tikslų, griežtų apribojimų, lankščių pageidavimų ir neišspręstų priskyrimų rodymą UI.
Peržiūrėti susijusias demonstracijasEtaloninis vertinimas / planuojama
Sąlygos sąžiningam sprendiklių palyginimui
Planuojama pastaba apie egzempliorių rinkinius, laiko ribas, optimalumo atotrūkius, atsitiktines sėklas ir aparatinę įrangą.
Peržiūrėti publikavimo kriterijusElementai „Rengiama“ nėra paskelbti straipsniai. Po publikavimo kiekviena pastaba gauna datą, šaltinį, autorių, atkūrimo kelią ir žinomus ribojimus.
DUK
Tyrimų, įrodymo įrankių ir verslo naudojimo ribos.
Šie punktai aiškiai nurodomi, kad tyrimų puslapiai nebūtų palaikyti gamybinėmis garantijomis.
Skaityti apie įmonę01 Ar Math Lab yra sutartinė kūrimo paslauga?
Ne. Tai vieta tyrimo požiūriui ir artefaktams skelbti. Pokalbiuose su klientais atskiriame taikomus metodus, metodus, kuriems reikia papildomos validacijos, ir tyrimo etapo temas.
02 Ar NPA gali pakeisti Lean arba Rocq?
Ne. Dabartinis NPA nėra praktinis Lean ar Rocq pakaitalas. Tai tyrimo ir įgyvendinimo projektas apie sertifikatus, nepriklausomą tikrinimą ir mažą patikimą bazę.
03 Ar DI sugeneruotais įrodymais pasitikite tokiais, kokie jie yra?
Ne. DI, paieška ir taktikos padeda generuoti kandidatus. Vertiname, ar galutinį sertifikatą priima nuo tų generavimo kelių nepriklausomas tikrintuvas.
04 Ar formalusis tikrinimas pašalina visas klaidas?
Ne. Formalieji metodai tikrina konkrečias savybes pagal aiškią specifikaciją. Neteisingos specifikacijos, už apimties ribų esantis kodas, operacijos ir išorinės paslaugos vis tiek turi būti peržiūrimos atskirai.
05 Ar tai susiję su verslo sistemų darbu?
Taip. Paprastai šią discipliną taikome palaipsniui: apribojimams, rezultatų priežastims, skaičiavimų istorijai, leidimų riboms ir svarbios verslo logikos patikroms.
Aptarti problemą
Galite aptarti spręstiną darbą, ne tik tyrimo temą.
Pradėkite nuo dabartinės skaičiuoklės, taisyklių ir vietų, kur sprendimus taiso žmonės. Galime sutvarkyti, kas turėtų būti pirmiau: matematinis modeliavimas, taisyklių automatizavimas ar prototipas.
Šaltinių momentinė kopija / 2026-06-21
Teiginiai apie NPA remiasi finitefield-org/npa repozitorijos momentine kopija. Lean ir Rocq pozicionavimas remiasi jų oficialiomis svetainėmis. Repozitorijos būsena, naujausios žymos ir metodo peržiūros formuluotės patikrintos 2026-06-28.