MPK Assurance / vurdering av bevisklarhet for Go-kode
Vi kontrollerer kritisk Go-logikk som flytter penger, for eksempel refusjoner, gebyrer, saldoer og reserver, mekanisk mot eksplisitte spesifikasjoner, antakelser og avgrensning. Gemini forbereder beviskandidater, og den uavhengige MPK-kjernen tar den endelige avgjørelsen.
Begrenset til de første 5 selskapene MPK-tilbud for tidlig bruk JPY 49 800(før skatt)
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 bryter egenskapen.
Kjernen godtok det korrigerte kanoniske sertifikatet.
30-sekundersdemo for refusjoner
Prøv den forberedte refusjonskoden og se flyten fra moteksempel til retting og vellykket bevis. Du trenger ikke legge inn konfidensiell kode i den offentlige demoen.
Refusjonspolicy: kumulative refusjoner må ikke overstige betalt beløp
Vi fant konkrete inndata der den kumulative refusjonen overstiger betalt beløp.
Resultatklassifisering
Den spesifiserte egenskapen holder under de eksplisitte antakelsene og avgrensningen.
BEVISTVi viser konkrete inndata som bryter egenskapen, og tydeliggjør hvilken betingelse som må rettes.
MOTBEVISTVi rapporterer tydelig når den gjeldende strategien ikke kan avgjøre om egenskapen holder.
UKJENTVi forklarer konkrete grunner til at målet ikke kan håndteres, for eksempel syntaks som ikke støttes, ekstern I/O eller atferd som ikke støttes.
IKKE ANVENDBARTForskjell fra testing
| Sammenligning | Test | Bevis |
|---|---|---|
| Mål | Utvalgte inndata | Spesifisert egenskap |
| Visning av moteksempel | △ | ○ |
| Etterprøving | Kjøringslogg | Sertifikat |
| Endelig vurdering | Testpakke | Kjerne |
Vi kontrollerer egenskapen mot eksplisitte spesifikasjoner, antakelser og omfang, ikke bare noen få eksempeldata.
Du kan starte med en kritisk Go-policyfunksjon som er isolert fra ekstern I/O.
AI forbereder bare kandidater. Endelig aksept utføres av en uavhengig kjerne som leser det kanoniske sertifikatet.
Gemini kjører bevisflyten, MPK tar tillitsbeslutningen, og et menneske godkjenner leveransen.
Dokumentasjonspakke
Vurdering av bevisklarhet
Kanonisk sertifikatoppføring
Vurdering av bevisklarhet
Dette er den planlagte standardprisen. Vi kjører nå en kampanje for tidlig bruk, begrenset til de første 5 selskapene, til JPY 49 800 før skatt.
MPK-tilbud for tidlig bruk
Begrenset til de første 5 selskapeneI MPK-vurderingen av bevisklarhet velger vi én målrettet Go-funksjon, definerer egenskapen som skal garanteres, genererer beviskandidater med AI og kjører en uavhengig kontroll med MPK-kjernen.
Dette tilbudet gjelder selskaper som kan gi ærlige tilbakemeldinger etter tjenesten og godkjenne en casestudie for publisering på MPKs offisielle nettsted. Casestudien kan inneholde selskapsnavn, kontaktnavn, tittel, tilbakemelding og enten et representativt bilde eller selskapslogo.
Tjenesteflyt
Bekreft feilscenarioet som kan føre til tap, og mål-funksjonen.
Lås funksjonen, egenskapen, antakelsene og ekskludert omfang.
AI forbereder kandidater, og MPK kontrollerer sertifikatet.
Gå gjennom beviset, moteksempelet, ukjent resultat, avgrensninger og dokumentasjon.
Avklar om arbeidet skal gå videre til rettinger, flere funksjoner eller CI/CD-integrasjon.
Vanlige spørsmål
Disse svarene dekker vanlige spørsmål før du kontakter oss, inkludert bevisomfang, AI-ens rolle og hvordan kode håndteres.
Nei. Vi kontrollerer bare den spesifiserte egenskapen innenfor eksplisitte antakelser, omfang og et støttet delsett av Go. Dette garanterer ikke hele applikasjonen eller eksterne systemer.
Ikke for den første gjennomgangen. Vi starter med å bekrefte en Go-policyfunksjon isolert fra ekstern I/O og egenskapen dere vil garantere.
Nei. Gemini lager egenskaper, bevisstrategier og beviskandidater. Den uavhengige MPK-kjernen godtar eller avviser det endelige sertifikatet.
Vi klassifiserer resultatet som moteksempel, ukjent eller utenfor omfang, og forklarer deretter årsaken, nødvendige spesifikasjoner, sannsynlige rettinger og hvordan en bevisbar enhet kan isoleres.
Etter at vurderingen av bevisklarhet har bekreftet målet og bevisbarheten, kan vi foreslå kontinuerlige kontroller eller CI/CD-integrasjon separat.
Du trenger ikke lime inn konfidensiell kode i det offentlige skjemaet. Etter henvendelsen avklarer vi NDA-håndtering og en sikker delingsmetode.
Kontakt
Fortell oss hvilken feil som ville bety mest, og hvilken Go-funksjon du vil ha vurdert. Du trenger ikke lime inn konfidensiell kode i det offentlige skjemaet.
NDA og sikker kodedeling støttes