Svojstvo za proveru
0 ≤ refunded + amount ≤ paid
- Cilj: jedna funkcija pravila povraćaja
- Ulazi: nenegativni celi brojevi
- Spoljni I/O, baza podataka i mreža su izvan opsega
- Provereno u okviru izričitih pretpostavki i podskupa Go jezika
MPK Assurance / pregled spremnosti za dokazivanje Go koda
Vaš Go kod dokazujemo
umesto da ga samo testiramo.
Mehanički proveravamo kritičnu Go logiku koja pomera novac, kao što su povraćaji, naknade, stanja i rezerve, prema izričitim specifikacijama, pretpostavkama i opsegu. Gemini priprema kandidate za dokaz, a nezavisni MPK kernel donosi konačnu odluku.
Ograničeno na prvih 5 kompanija MPK ponuda za rano usvajanje JPY 49,800(bez poreza)Počnite jednom Go funkcijom
Do 2 svojstva
Bez javnog unosa
poverljivog koda
poverljivog koda
Isporuka
ponovo proverljivih dokaza
ponovo proverljivih 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 PROVERU
∀ paid, refunded, amount:
0 ≤ refunded + amount ≤ paid
PRONAĐEN KONTRAPRIMER
paid=100, refunded=80, amount=30 narušava svojstvo.
KERNEL POTVRDIO
Kernel je prihvatio ispravljeni kanonski sertifikat.
Provera izvan testiranjaPočnite od običnog Go kodaOdvojite AI od odluka o poverenjuPrikažite dokaz, kontraprimere i isključenja
Demo povraćaja od 30 sekundi
Pronađite kontraprimer, zatim dokažite ispravljenu verziju.
Isprobajte pripremljeni kod za povraćaj i pogledajte tok od kontraprimera do ispravke i uspešnog dokaza. Poverljiv kod ne morate unositi u javni demo.
Pravilo povraćaja: ukupni povraćaji ne smeju premašiti plaćeni iznos
Rezultat provere (implementacija sa greškom)
Pronađen kontraprimer
Pronašli smo konkretne ulaze kod kojih ukupni povraćaj premašuje plaćeni iznos.
paid = 100
refunded = 80
amount = 30
rezultat = 110 (narušavanje svojstva)
refunded = 80
amount = 30
rezultat = 110 (narušavanje svojstva)
Tehnički detalji
- ID izvršavanja
- run_refund_bug_20260727
- Hash sertifikata
- — nije generisan jer je pronađen kontraprimer
- Odluka kernela
- ODBIJENO / KONTRAPRIMER
- Izveštaj o aksiomima
- aritmetika celih brojeva / izričite pretpostavke
Klasifikacija rezultata
Četiri tipa rezultata
Dokazano
Zadato svojstvo važi pod izričitim pretpostavkama i u zadatom opsegu.
DOKAZANOPronađen kontraprimer
Prikazujemo konkretne ulaze koji narušavaju svojstvo i objašnjavamo koji uslov treba ispraviti.
OPOVRGNUTONepoznato
Jasno navodimo kada trenutna strategija ne može da utvrdi da li svojstvo važi.
NEPOZNATOIzvan opsega
Objašnjavamo konkretne razloge zbog kojih cilj ne možemo obraditi, na primer nepodržanu sintaksu, spoljni I/O ili nepodržano ponašanje.
NIJE PRIMENLJIVORazlika u odnosu na testiranje
Proveravamo zadato svojstvo, a ne samo odabrane ulaze.
Testiranje na primerima
- Pokreće slučajeve koje ste napisali
- Ne pokriva neodabrane ulaze
- Prolazan rezultat nije sertifikat
- Poverenje zavisi od dizajna testova
MPK Assurance (dokaz)
- Proverava zadana svojstva i opseg
- Prikazuje konkretne ulaze koji ruše svojstvo
- Ostavlja ponovo proverljiv sertifikat i hash
- Nezavisni kernel donosi konačnu odluku
| Poređenje | Testiranje | Dokaz |
|---|---|---|
| Cilj | Odabrani ulazi | Zadato svojstvo |
| Prikaz kontraprimera | △ | ○ |
| Ponovna provera | Zapis izvršavanja | Sertifikat |
| Konačna odluka | Skup testova | Kernel |
3 karakteristike
Provera izvan testiranja
Svojstvo proveravamo prema izričitim specifikacijama, pretpostavkama i opsegu, a ne samo na nekoliko probnih ulaza.
Koristite Go, a ne poseban jezik za dokaze
Možete početi kritičnom Go funkcijom poslovnog pravila izolovanom od spoljnog I/O-a.
Neka AI dokazuje, ali se ne oslanjajte na AI
AI samo priprema kandidate. Konačno prihvatanje obavlja nezavisni kernel koji čita kanonski sertifikat.
Neka AI obavi posao. Ne dozvolite da AI donese konačnu odluku.
KlijentPredaje Go funkciju i svojstvo koje treba garantovati
GeminiPredlaže svojstva, strategiju i kandidate za dokaz
MPKGranica poverenja koja nezavisno proverava sertifikate
ČovekPotvrđuje specifikacije, pretpostavke i poverljivost
Paket dokazaIsporučuje paket dokaza koji se može ponovo proveriti
Gemini izvodi tok dokazivanja, MPK donosi odluku o poverenju, a čovek odobrava isporuku.
Slučajevi u kojima provera pomaže
PovraćajiUkupni povraćaji ne smeju premašiti plaćeni iznos
NaknadeNikada negativne i nikada iznad ugovornih ograničenja
RezerveStanje posle obrade ne pada ispod minimuma
PopustiOstaju u granicama čak i kada se popusti sabiraju
PoeniIzdati poeni ne premašuju budžetsko ograničenje
RaspodelaRaspodeljeni iznosi se sabiraju do izvornog glavnog iznosa
Paket dokaza
Isporučujemo dokaze koji se mogu ponovo proveriti, a ne odgovor AI-ja.
FINITE FIELD
MPK SERTIFIKAT
Pregled spremnosti za dokazivanje
Kanonski zapis sertifikata
ODLUKA KERNELA
PRIHVAĆENO
PRIHVAĆENO
MPK
- Hash sertifikata
- Odluka MPK kernela
- Rezultat Go referentnog proverivača
- Izveštaj o aksiomima
- Dokazana svojstva i navedene pretpostavke
- Isključeni opseg i razlozi izvan opsega
- Kontraprimer, ako je pronađen
- ID izvršavanja i informacije za ponovnu proveru
Pregled spremnosti za dokazivanje
Pregledajte prvu funkciju u fiksnom opsegu.
JPY 198,000 (bez poreza)
- Jedna Go funkcija
- Do 2 svojstva za dokazivanje
- Klasifikuje rezultate kao dokazano, kontraprimer, nepoznato ili izvan opsega
- Paket dokaza i onlajn prolazak kroz rezultate
Ovo je planirana standardna cena. Trenutno sprovodimo kampanju za rano usvajanje ograničenu na prvih 5 kompanija po ceni JPY 49,800 bez poreza.
MPK ponuda za rano usvajanje
Ograničeno na prvih 5 kompanijaProverite da li se vaš kritični Go kod može dokazati, a ne samo testirati.
U MPK pregledu spremnosti za dokazivanje biramo jednu ciljnu Go funkciju, definišemo svojstvo koje treba garantovati, generišemo kandidate za dokaz uz pomoć AI-ja i pokrećemo nezavisnu proveru MPK kernelom.
Šta je uključeno
- Jedna Go funkcija
- Do 2 svojstva za dokazivanje
- Procena kompatibilnosti sa MPK
- Izveštaj o dokazima, kontraprimerima, preprekama za dokazivanje i stavkama izvan opsega
- Izveštaj koji sažima opseg dokaza i pretpostavke
Uslovi kampanje
Ova ponuda je namenjena kompanijama koje mogu dati iskrene povratne informacije nakon usluge i odobriti studiju slučaja za objavu na zvaničnoj MPK stranici. Studija slučaja može uključiti naziv kompanije, ime osobe za kontakt, funkciju, povratne informacije i reprezentativnu fotografiju ili logotip kompanije.
Naziv kompanijeImeFunkcijaPovratne informacijeReprezentativna fotografija ili logotip kompanije
Pregledaćete sadržaj pre objave i koristićemo samo odobreni materijal. Ne tražimo pozitivnu recenziju.
Tok usluge
Tok usluge (5 koraka)
Otkrivanje
Potvrđujemo scenario kvara koji bi mogao izazvati gubitak i ciljnu funkciju.
Zaključavanje opsega
Zaključavamo funkciju, svojstvo, pretpostavke i isključeni opseg.
Pregled Gemini + MPK
AI priprema kandidate, a MPK proverava sertifikat.
Prolazak kroz rezultate
Prolazimo kroz dokaz, kontraprimer, nepoznat rezultat, isključenja i dokaze.
Sledeći koraci
Razjašnjavamo da li treba preći na ispravke, dodatne funkcije ili CI/CD integraciju.
Najbolje odgovara
- Implementirate logiku povraćaja, naknada ili stanja u Go jeziku
- Jedan nedostatak mogao bi izazvati finansijski gubitak ili revizijsko opterećenje
- Nemate poseban tim za formalnu verifikaciju
- Imate malu funkciju koja se može izolovati od spoljnog I/O-a
Trenutna ograničenja
- Dokazivanje proizvoljne cele Go aplikacije
- Celovita obrada koja uključuje bazu podataka, API-je, mrežu ili korisnički interfejs
- Otkrivanje svake bezbednosne ranjivosti
- Nepodržana sintaksa, spoljne zavisnosti ili nejasne specifikacije
FAQ
Česta pitanja pre prve konsultacije
Ovi odgovori pokrivaju česta pitanja pre nego što nam se obratite, uključujući opseg dokaza, ulogu AI-ja i način rukovanja kodom.
Da li ovo uklanja sve greške?
Ne. Zadato svojstvo proveravamo samo u okviru izričitih pretpostavki, opsega i podržanog Go podskupa. To ne garantuje celu aplikaciju niti spoljne sisteme.
Da li treba da naučimo Lean ili Rocq?
Ne za prvi pregled. Počinjemo potvrdom Go funkcije poslovnog pravila izolovane od spoljnog I/O-a i svojstva koje želite garantovati.
Da li AI odlučuje šta je ispravno?
Ne. Gemini kreira svojstva, strategije dokazivanja i kandidate za dokaz. Nezavisni MPK kernel prihvata ili odbija konačni sertifikat.
Šta se dešava ako dokaz ne uspe?
Rezultat klasifikujemo kao kontraprimer, nepoznato ili izvan opsega, zatim objašnjavamo razlog, potrebne specifikacije, verovatne ispravke i kako izolovati jedinicu koju je moguće dokazati.
Može li se ovo integrisati u CI/CD?
Nakon što pregled spremnosti za dokazivanje potvrdi cilj i izvodljivost dokaza, možemo zasebno predložiti kontinuirane provere ili CI/CD integraciju.
Da li treba da pošaljemo kod uz upit?
Poverljiv kod ne morate lepiti u javni obrazac. Nakon upita potvrdićemo postupanje prema NDA-u i bezbedan način deljenja.
Kontakt
Proverite da li se vaš kod može dokazati.
Recite nam koji bi kvar bio najvažniji i koju Go funkciju želite da pregledamo. Poverljiv kod ne morate lepiti u javni obrazac.
Podržani su NDA i bezbedno deljenje koda