MPK Assurance / parathedstjek for Go-bevis
Vi kontrollerer mekanisk kritisk Go-logik, der flytter penge, f.eks. refunderinger, gebyrer, saldi og reserver, mod tydelige specifikationer, antagelser og afgrænsning. Gemini forbereder beviskandidater, og den uafhængige MPK-kerne træffer den endelige afgørelse.
Begrænset til de første 5 virksomheder MPK-tilbud for tidlige brugere JPY 49,800(ekskl. moms)
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
}∀ paid, refunded, amount:
0 ≤ refunded + amount ≤ paid
paid=100, refunded=80, amount=30 bryder egenskaben.
Kernen accepterede det rettede kanoniske certifikat.
30-sekundersdemo om refundering
Prøv den forberedte refunderingskode, og se forløbet fra modbevis til rettelse og vellykket bevis. Du behøver ikke indtaste fortrolig kode i den offentlige demo.
Refunderingsregel: samlede refunderinger må ikke overstige det betalte beløb
Vi fandt konkrete input, hvor den samlede refundering overstiger det betalte beløb.
Resultatklassificering
Den angivne egenskab holder under de tydelige antagelser og den aftalte afgrænsning.
BEVISTVi viser konkrete input, der bryder egenskaben, og præciserer hvilken betingelse der skal rettes.
MODBEVISTVi rapporterer tydeligt, når den aktuelle strategi ikke kan afgøre, om egenskaben holder.
UKENDTVi forklarer konkret, hvorfor målet ikke kan håndteres, f.eks. syntaks, ekstern I/O eller adfærd, der ikke understøttes.
IKKE ANVENDELIGTForskel fra test
| Sammenligning | Test | Bevis |
|---|---|---|
| Mål | Udvalgte input | Angivet egenskab |
| Visning af modbevis | △ | ○ |
| Genkontrol | Kørselslog | Certifikat |
| Endelig vurdering | Testsamling | Kerne |
Vi kontrollerer egenskaben mod tydelige specifikationer, antagelser og afgrænsning, ikke kun nogle få eksempelinput.
Du kan starte med en kritisk Go-regelfunktion, der er isoleret fra ekstern I/O.
AI forbereder kun kandidater. Den endelige accept udføres af en uafhængig kerne, der læser det kanoniske certifikat.
Gemini kører bevisarbejdet, MPK træffer tillidsafgørelsen, og et menneske godkender leverancen.
Dokumentationspakke
Parathedstjek for bevis
Kanonisk certifikatpost
Parathedstjek for bevis
Dette er den planlagte normalpris. Vi kører i øjeblikket en kampagne for tidlige brugere, begrænset til de første 5 virksomheder, til JPY 49,800 ekskl. moms.
MPK-tilbud for tidlige brugere
Begrænset til de første 5 virksomhederI MPK-parathedstjekket for bevis vælger vi én Go-målfunktion, definerer egenskaben der skal garanteres, genererer beviskandidater med AI og kører en uafhængig kontrol med MPK-kernen.
Tilbuddet er for virksomheder, der kan give ærlig tilbagemelding efter serviceforløbet og godkende en kundecase til offentliggørelse på MPK's officielle website. Casen kan omfatte firmanavn, kontaktpersonens navn, titel, tilbagemelding og enten et repræsentativt foto eller virksomhedens logo.
Serviceforløb
Bekræft fejlscenariet, der kan give tab, og den funktion der skal gennemgås.
Fastlæg funktion, egenskab, antagelser og udeladt afgrænsning.
AI forbereder kandidater, og MPK kontrollerer certifikatet.
Gennemgå bevis, modbevis, ukendt resultat, afgrænsninger og dokumentation.
Afklar om næste skridt er rettelser, flere funktioner eller CI/CD-integration.
FAQ
Svarene dækker almindelige spørgsmål før kontakt, herunder bevisets afgrænsning, AI's rolle og håndtering af kode.
Nej. Vi kontrollerer kun den angivne egenskab under de tydelige antagelser, den aftalte afgrænsning og den understøttede delmængde af Go. Det garanterer ikke hele applikationen eller eksterne systemer.
Ikke til den første gennemgang. Vi starter med at bekræfte en Go-regelfunktion, der er isoleret fra ekstern I/O, og den egenskab I vil garantere.
Nej. Gemini opretter egenskaber, bevisstrategier og beviskandidater. Den uafhængige MPK-kerne accepterer eller afviser det endelige certifikat.
Vi klassificerer resultatet som modbevis, ukendt eller uden for afgrænsningen og forklarer derefter årsagen, nødvendige specifikationer, sandsynlige rettelser og hvordan en bevisbar enhed kan isoleres.
Når parathedstjekket har bekræftet mål og bevisbarhed, kan vi separat foreslå løbende kontroller eller CI/CD-integration.
I behøver ikke indsætte fortrolig kode i den offentlige formular. Efter forespørgslen bekræfter vi NDA-håndtering og en sikker delingsmetode.
Kontakt
Fortæl os, hvilken fejl der vil betyde mest, og hvilken Go-funktion I vil have gennemgået. I behøver ikke indsætte fortrolig kode i den offentlige formular.
NDA og sikker kodedeling understøttes