MPK Assurance / bewijsbaarheidsbeoordeling van Go-code
We controleren kritieke Go-logica die geld verplaatst, zoals terugbetalingen, kosten, saldi en reserves, formeel tegen expliciete specificaties, aannames en reikwijdte. Gemini bereidt bewijskandidaten voor en de onafhankelijke MPK-kernel neemt het eindoordeel.
Beperkt tot de eerste 5 bedrijven MPK-aanbod voor vroege gebruikers JPY 49.800(excl. btw)
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 schendt de eigenschap.
De kernel accepteerde het gecorrigeerde canonieke certificaat.
Terugbetalingsdemo van 30 seconden
Probeer de voorbereide terugbetalingscode en zie de stroom van tegenvoorbeeld naar correctie en geslaagd bewijs. U hoeft geen vertrouwelijke code in de openbare demo in te voeren.
Terugbetalingsbeleid: cumulatieve terugbetalingen mogen het betaalde bedrag niet overschrijden
We vonden concrete invoer waarbij de cumulatieve terugbetaling het betaalde bedrag overschrijdt.
Resultaatclassificatie
De opgegeven eigenschap geldt onder de expliciete aannames en reikwijdte.
BEWEZENWe tonen concrete invoer die de eigenschap schendt en verduidelijken welke voorwaarde moet worden gecorrigeerd.
WEERLEGDWe rapporteren duidelijk wanneer de huidige strategie niet kan bepalen of de eigenschap geldt.
ONBEKENDWe leggen concreet uit waarom we het doel niet kunnen behandelen, zoals niet-ondersteunde syntaxis, externe I/O of niet-ondersteund gedrag.
BUITEN REIKWIJDTEVerschil met testen
| Vergelijking | Testen | Bewijs |
|---|---|---|
| Doel | Geselecteerde invoer | Opgegeven eigenschap |
| Tegenvoorbeeld tonen | △ | ○ |
| Opnieuw controleren | Uitvoeringslog | Certificaat |
| Eindoordeel | Testsuite | Kernel |
We controleren de eigenschap tegen expliciete specificaties, aannames en reikwijdte, niet alleen met enkele voorbeeldinvoer.
U kunt beginnen met een kritieke Go-beleidsfunctie die van externe I/O is geïsoleerd.
AI bereidt alleen kandidaten voor. De uiteindelijke acceptatie gebeurt door een onafhankelijke kernel die het canonieke certificaat leest.
Gemini voert de bewijsworkflow uit, MPK neemt de vertrouwensbeslissing en een mens keurt de oplevering goed.
Bewijspakket
Bewijsbaarheidsbeoordeling
canoniek certificaatrecord
Bewijsbaarheidsbeoordeling
Dit is de geplande standaardprijs. Momenteel loopt er een vroege-gebruikerscampagne voor de eerste 5 bedrijven, voor JPY 49.800 exclusief btw.
MPK-aanbod voor vroege gebruikers
Beperkt tot de eerste 5 bedrijvenIn de MPK-bewijsbaarheidsbeoordeling kiezen we één doelgerichte Go-functie, definiëren we de te garanderen eigenschap, genereren we bewijskandidaten met AI en voeren we een onafhankelijke controle uit met de MPK-kernel.
Dit aanbod is bedoeld voor bedrijven die na de dienst publiek bruikbare feedback kunnen geven en een casestudy voor publicatie op de officiële MPK-site kunnen goedkeuren. De casestudy kan de bedrijfsnaam, contactpersoon, functie, feedback en een representatieve foto of bedrijfslogo bevatten.
Proces
Bevestig het faalscenario dat schade kan veroorzaken en de doelfunctie.
Leg de functie, eigenschap, aannames en uitgesloten reikwijdte vast.
AI bereidt kandidaten voor en MPK controleert het certificaat.
Neem bewijs, tegenvoorbeeld, onbekend resultaat, uitsluitingen en bewijsmateriaal door.
Bepaal of de volgende stap correcties, extra functies of CI/CD-integratie is.
FAQ
Deze antwoorden behandelen veelgestelde vragen voordat u contact opneemt, waaronder de bewijsreikwijdte, de rol van AI en de omgang met code.
Nee. We controleren de opgegeven eigenschap alleen binnen de expliciete aannames, reikwijdte en ondersteunde Go-subset. Dit garandeert niet de volledige applicatie of externe systemen.
Niet voor de eerste beoordeling. We beginnen met het bevestigen van een Go-beleidsfunctie die van externe I/O is geïsoleerd en de eigenschap die u wilt garanderen.
Nee. Gemini maakt eigenschappen, bewijsstrategieën en bewijskandidaten. De onafhankelijke MPK-kernel accepteert of verwerpt het uiteindelijke certificaat.
We classificeren het resultaat als tegenvoorbeeld, onbekend of buiten de reikwijdte en leggen daarna de reden, benodigde specificaties, waarschijnlijke correcties en isolatie van een bewijsbare eenheid uit.
Nadat de bewijsbaarheidsbeoordeling het doel en de bewijsbaarheid bevestigt, kunnen we afzonderlijk continue controles of CI/CD-integratie voorstellen.
U hoeft geen vertrouwelijke code in het openbare formulier te plakken. Na uw aanvraag bevestigen we de NDA-afhandeling en een veilige manier om code te delen.
Contact
Vertel ons welk faalscenario het belangrijkst is en welke Go-functie u wilt laten beoordelen. U hoeft geen vertrouwelijke code in het openbare formulier te plakken.
NDA en veilig delen van code ondersteund