Svojstvo za provjeru
0 ≤ refunded + amount ≤ paid
- Cilj: jedna funkcija pravila povrata
- Ulazi: nenegativni cijeli brojevi
- Vanjski I/O, baza podataka i mreža izvan su opsega
- Provjereno unutar izričitih pretpostavki i podskupa Go jezika
MPK Assurance / provjera spremnosti za dokaz Go koda
Vaš Go kod dokazujemo
umjesto da ga samo testiramo.
Mehanički provjeravamo kritičnu Go logiku koja premješta novac, kao što su povrati, naknade, salda i rezerve, prema izričitim specifikacijama, pretpostavkama i opsegu. Gemini priprema kandidate za dokaz, a neovisna MPK jezgra donosi konačnu odluku.
Ograničeno na prvih 5 tvrtki MPK ponuda za rane korisnike JPY 49,800(bez poreza)Počnite jednom Go funkcijom
Do 2 svojstva
Bez javnog unosa
povjerljivog koda
povjerljivog koda
Isporuka
ponovno provjerljivih dokaza
ponovno provjerljivih dokaza
refund.go
func ApplyRefund(paid, refunded, amount int64) (int64, error) {
if amount < 0 {
return refunded, errors.New("negative amount")
}
if refunded+amount > paid {
return refunded, errors.New("exceeds paid")
}
return refunded + amount, nil
}SVOJSTVO ZA PROVJERU
∀ paid, refunded, amount:
0 ≤ refunded + amount ≤ paid
PRONAĐEN PROTUPRIMJER
paid=100, refunded=80, amount=30 krši svojstvo.
JEZGRA POTVRDILA
Jezgra je prihvatila ispravljeni kanonski certifikat.
Jamstvo izvan testiranjaPočnite od običnog Go kodaOdvojite AI od odluka o povjerenjuPrikažite dokaz, protuprimjere i izuzeća
Demonstracija povrata od 30 sekundi
Pronađite protuprimjer, zatim dokažite ispravljenu verziju.
Isprobajte pripremljeni kod za povrat i pogledajte tijek od protuprimjera do ispravka i uspješnog dokaza. U javnu demonstraciju ne morate unositi povjerljivi kod.
Pravilo povrata: kumulativni povrati ne smiju premašiti plaćeni iznos
Rezultat provjere (neispravna implementacija)
Pronađen protuprimjer
Pronašli smo konkretne ulaze kod kojih kumulativni povrat premašuje plaćeni iznos.
paid = 100
refunded = 80
amount = 30
rezultat = 110 (kršenje svojstva)
refunded = 80
amount = 30
rezultat = 110 (kršenje svojstva)
Tehnički detalji
- ID izvršavanja
- run_refund_bug_20260727
- Hash certifikata
- — nije generiran jer je pronađen protuprimjer
- Odluka jezgre
- ODBIJENO / PROTUPRIMJER
- Izvješće o aksiomima
- aritmetika cijelih brojeva / izričite pretpostavke
Klasifikacija rezultata
Četiri vrste rezultata
Dokazano
Zadano svojstvo vrijedi pod izričitim pretpostavkama i u zadanom opsegu.
DOKAZANOPronađen protuprimjer
Prikazujemo konkretne ulaze koji krše svojstvo i pojašnjavamo koji uvjet treba ispraviti.
OPOVRGNUTONepoznato
Jasno izvješćujemo kada trenutačna strategija ne može utvrditi vrijedi li svojstvo.
NEPOZNATOIzvan opsega
Objašnjavamo konkretne razloge zašto cilj ne možemo obraditi, primjerice nepodržanu sintaksu, vanjski I/O ili nepodržano ponašanje.
NIJE PRIMJENJIVORazlika u odnosu na testiranje
Provjeravamo zadano svojstvo, a ne samo odabrane ulaze.
Testiranje na primjerima
- Pokreće slučajeve koje ste napisali
- Ne pokriva neodabrane ulaze
- Prolazan rezultat nije certifikat
- Povjerenje ovisi o dizajnu testova
MPK Assurance (dokaz)
- Provjerava zadana svojstva i opseg
- Prikazuje konkretne ulaze koji ruše svojstvo
- Ostavlja ponovno provjerljiv certifikat i hash
- Neovisna jezgra donosi konačnu odluku
| Usporedba | Testiranje | Dokaz |
|---|---|---|
| Cilj | Odabrani ulazi | Zadano svojstvo |
| Prikaz protuprimjera | △ | ○ |
| Ponovna provjera | Zapis izvršavanja | Certifikat |
| Konačna odluka | Skup testova | Jezgra |
3 značajke
Jamstvo izvan testiranja
Svojstvo provjeravamo prema izričitim specifikacijama, pretpostavkama i opsegu, a ne samo na nekoliko oglednih ulaza.
Koristite Go, a ne poseban jezik za dokaze
Možete početi kritičnom Go funkcijom poslovnog pravila izoliranom od vanjskog I/O-a.
Neka AI dokazuje, ali ne vjerujte AI-ju
AI samo priprema kandidate. Konačno prihvaćanje obavlja neovisna jezgra koja čita kanonski certifikat.
Neka AI obavi posao. Ne dopustite da AI donese konačnu odluku.
KlijentPredaje Go funkciju i svojstvo koje treba zajamčiti
GeminiPredlaže svojstva, strategiju i kandidate za dokaz
MPKGranica povjerenja koja neovisno provjerava certifikate
ČovjekPotvrđuje specifikacije, pretpostavke i povjerljivost
Dokazni paketIsporučuje ponovno provjerljiv paket dokaza
Gemini izvodi tijek dokazivanja, MPK donosi odluku o povjerenju, a čovjek odobrava isporuku.
Slučajevi u kojima provjera pomaže
PovratiKumulativni povrati ne smiju premašiti plaćeni iznos
NaknadeNikad negativne i nikad iznad ugovornih ograničenja
RezerveSaldo nakon obrade ne pada ispod minimuma
PopustiOstaje unutar granica i kada se popusti zbrajaju
BodoviIzdani bodovi ne premašuju proračunsko ograničenje
RaspodjelaRaspodijeljeni iznosi zbrajaju se do izvornog glavnog iznosa
Paket dokaza
Isporučujemo ponovno provjerljive dokaze, a ne odgovor AI-ja.
FINITE FIELD
MPK CERTIFIKAT
Provjera spremnosti za dokaz
Kanonski zapis certifikata
ODLUKA JEZGRE
PRIHVAĆENO
PRIHVAĆENO
MPK
- Hash certifikata
- Odluka MPK jezgre
- Rezultat Go referentnog provjerivača
- Izvješće o aksiomima
- Dokazana svojstva i navedene pretpostavke
- Isključeni opseg i razlozi izvan opsega
- Protuprimjer, ako je pronađen
- ID izvršavanja i informacije za ponovnu provjeru
Provjera spremnosti za dokaz
Pregledajte prvu funkciju unutar fiksnog opsega.
JPY 198,000 (bez poreza)
- Jedna Go funkcija
- Do 2 svojstva za dokazivanje
- Klasificira rezultate kao dokazano, protuprimjer, nepoznato ili izvan opsega
- Paket dokaza i mrežni prolazak kroz rezultate
To je planirana standardna cijena. Trenutačno provodimo kampanju za rane korisnike ograničenu na prvih 5 tvrtki po cijeni JPY 49,800 bez poreza.
MPK ponuda za rane korisnike
Ograničeno na prvih 5 tvrtkiProvjerite može li se vaš kritični Go kod dokazati, a ne samo testirati.
U MPK provjeri spremnosti za dokaz biramo jednu ciljnu Go funkciju, definiramo svojstvo koje treba zajamčiti, generiramo kandidate za dokaz uz pomoć AI-ja i pokrećemo neovisnu provjeru MPK jezgrom.
Što je uključeno
- Jedna Go funkcija
- Do 2 svojstva za dokazivanje
- Procjena kompatibilnosti s MPK-om
- Izvješće o dokazima, protuprimjerima, zaprekama dokazivanju i stavkama izvan opsega
- Izvješće koje sažima opseg dokaza i pretpostavke
Uvjeti kampanje
Ova ponuda namijenjena je tvrtkama koje mogu dati iskrene povratne informacije nakon usluge i odobriti studiju slučaja za objavu na službenoj MPK stranici. Studija slučaja može uključivati naziv tvrtke, ime kontakt osobe, poziciju, povratne informacije te reprezentativnu fotografiju ili logotip tvrtke.
Naziv tvrtkeImePozicijaPovratne informacijeReprezentativna fotografija ili logotip tvrtke
Pregledat ćete sadržaj prije objave, a koristit ćemo samo odobreni materijal. Ne tražimo pozitivnu recenziju.
Tijek usluge
Tijek usluge (5 koraka)
Otkrivanje
Potvrđujemo scenarij kvara koji bi mogao uzrokovati gubitak i ciljnu funkciju.
Zaključavanje opsega
Zaključavamo funkciju, svojstvo, pretpostavke i isključeni opseg.
Pregled Gemini + MPK
AI priprema kandidate, a MPK provjerava certifikat.
Prolazak kroz rezultate
Prolazimo kroz dokaz, protuprimjer, nepoznat rezultat, izuzeća i dokaze.
Sljedeći koraci
Razjašnjavamo treba li prijeći na ispravke, dodatne funkcije ili CI/CD integraciju.
Najbolje odgovara
- Implementirate logiku povrata, naknada ili salda u Go jeziku
- Jedan nedostatak mogao bi uzrokovati financijski gubitak ili revizijsko opterećenje
- Nemate poseban tim za formalnu verifikaciju
- Imate malu funkciju koja se može izolirati od vanjskog I/O-a
Trenutačna ograničenja
- Dokazivanje proizvoljne cjelovite Go aplikacije
- Cjelovita obrada koja uključuje bazu podataka, API-je, mrežu ili korisničko sučelje
- Otkrivanje svake sigurnosne ranjivosti
- Nepodržana sintaksa, vanjske ovisnosti ili nejasne specifikacije
FAQ
Česta pitanja prije prve konzultacije
Ovi odgovori pokrivaju česta pitanja prije nego što nam se obratite, uključujući opseg dokaza, ulogu AI-ja i način rukovanja kodom.
Uklanja li to sve greške?
Ne. Zadano svojstvo provjeravamo samo unutar izričitih pretpostavki, opsega i podržanog Go podskupa. To ne jamči cijelu aplikaciju ni vanjske sustave.
Moramo li naučiti Lean ili Rocq?
Ne za prvi pregled. Počinjemo potvrdom Go funkcije poslovnog pravila izolirane od vanjskog I/O-a i svojstva koje želite zajamčiti.
Odlučuje li AI što je ispravno?
Ne. Gemini stvara svojstva, strategije dokazivanja i kandidate za dokaz. Neovisna MPK jezgra prihvaća ili odbija konačni certifikat.
Što se događa ako dokaz ne uspije?
Rezultat klasificiramo kao protuprimjer, nepoznato ili izvan opsega, zatim objašnjavamo razlog, potrebne specifikacije, vjerojatne ispravke i kako izolirati jedinicu koju je moguće dokazati.
Može li se to integrirati u CI/CD?
Nakon što provjera spremnosti za dokaz potvrdi cilj i izvedivost dokaza, možemo zasebno predložiti kontinuirane provjere ili CI/CD integraciju.
Moramo li poslati kod uz upit?
Povjerljivi kod ne morate lijepiti u javni obrazac. Nakon upita potvrdit ćemo postupanje prema NDA-u i siguran način dijeljenja.
Kontakt
Provjerite može li se vaš kod dokazati.
Recite nam koji bi kvar bio najvažniji i koju Go funkciju želite pregledati. Povjerljivi kod ne morate lijepiti u javni obrazac.
Podržani su NDA i sigurno dijeljenje koda