MPK Assurance / Kontrola připravenosti důkazu pro Go

Váš kód v Go dokazujeme,
nejen testujeme.

Kritickou logiku v Go, která přesouvá peníze, například refundace, poplatky, zůstatky a rezervy, mechanicky kontrolujeme proti výslovným specifikacím, předpokladům a rozsahu. Gemini připraví kandidáty důkazu a nezávislé jádro MPK vydá konečný verdikt.

Vyzkoušet 30sekundovou ukázku refundace Požádat o kontrolu připravenosti důkazu

Pouze pro prvních 5 firem Nabídka MPK pro první nasazení 49 800 JPY(bez daně)

Začněte jednou funkcí v Go

Až 2 vlastnosti

Žádné veřejné zadávání
důvěrného kódu

Dodáme
znovu ověřitelné důkazy

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
}

VLASTNOST K OVĚŘENÍ

∀ paid, refunded, amount:
0 ≤ refunded + amount ≤ paid

NALEZEN PROTIPŘÍKLAD

paid=100, refunded=80, amount=30 porušuje vlastnost.

JÁDRO OVĚŘENO

Jádro přijalo opravený kanonický certifikát.

Jistota nad rámec testůZačněte běžným GoOddělte AI od rozhodnutí o důvěřeUkažte důkaz, protipříklady a vyloučení

30sekundová ukázka refundace

Najděte protipříklad a potom dokažte opravenou verzi.

Vyzkoušejte připravený kód refundace a projděte tok od protipříkladu přes opravu až k úspěšnému důkazu. Do veřejné ukázky nemusíte zadávat důvěrný kód.

Zásada refundace: součet refundací nesmí překročit zaplacenou částku

Ověřovaná vlastnost

0 ≤ refunded + amount ≤ paid

Cíl: jedna funkce zásad refundace
Vstupy: nezáporná celá čísla
Externí I/O, DB a síť jsou mimo rozsah
Kontrolováno v rámci výslovných předpokladů a podmnožiny Go

Výsledek ověření (chybná implementace)

Nalezen protipříklad

Našli jsme konkrétní vstupy, při kterých součet refundací překročí zaplacenou částku.

paid = 100
refunded = 80
amount = 30
výsledek = 110 (porušení vlastnosti)

Technické detaily

ID běhu: run_refund_bug_20260727
Hash certifikátu: — nevygenerováno, protože byl nalezen protipříklad
Verdikt jádra: ODMÍTNUTO / PROTIPŘÍKLAD
Zpráva o axiomech: celočíselná aritmetika / výslovné předpoklady

Klasifikace výsledku

Čtyři typy výsledků

Dokázáno

Zadaná vlastnost platí při výslovných předpokladech a rozsahu.

DOKÁZÁNO

Nalezen protipříklad

Ukážeme konkrétní vstupy, které vlastnost porušují, a vyjasníme podmínku, kterou je třeba opravit.

VYVRÁCENO

Neznámé

Jasně uvedeme, když aktuální strategie nedokáže určit, zda vlastnost platí.

NEZNÁMÉ

Mimo rozsah

Vysvětlíme konkrétní důvody, proč cíl nemůžeme zpracovat, například nepodporovanou syntaxi, externí I/O nebo nepodporované chování.

NELZE POUŽÍT

Rozdíl oproti testování

Kontrolujeme zadanou vlastnost, ne jen vybrané vstupy.

Testování (na příkladech)

Spouští případy, které jste napsali
Nevybrané vstupy zůstávají nepokryté
Úspěšný výsledek není certifikát
Důvěra závisí na návrhu testů

MPK Assurance (důkaz)

Kontroluje zadané vlastnosti a rozsah
Ukazuje konkrétní vstupy, které vlastnost porušují
Zanechá znovu ověřitelný certifikát a hash
Konečný verdikt vydává nezávislé jádro

Porovnání	Testování	Důkaz
Cíl	Vybrané vstupy	Zadaná vlastnost
Zobrazení protipříkladu	△	○
Opětovná kontrola	Protokol spuštění	Certifikát
Konečný úsudek	Testovací sada	Jádro

3 vlastnosti

Jistota nad rámec testů

Vlastnost kontrolujeme proti výslovným specifikacím, předpokladům a rozsahu, nejen proti několika ukázkovým vstupům.

Použijte Go, ne speciální jazyk pro důkazy

Můžete začít kritickou funkcí zásad v Go izolovanou od externího I/O.

Nechte AI dokazovat, ale nedůvěřujte jí

AI pouze připravuje kandidáty. Konečné přijetí provádí nezávislé jádro, které čte kanonický certifikát.

Nechte AI odvést práci. Nenechte AI vydat konečný úsudek.

ZákazníkPředá funkci v Go a vlastnost, kterou je třeba zaručit

GeminiNavrhne vlastnosti, strategii a kandidáty důkazu

MPKHranice důvěry, která nezávisle kontroluje certifikáty

ČlověkPotvrdí specifikace, předpoklady a důvěrnost

DůkazyDodá znovu ověřitelný balíček důkazů

Gemini provádí důkazový tok, MPK rozhoduje o důvěře a člověk schvaluje dodání.

Případy, kde ověření pomáhá

RefundaceSoučet refundací nesmí překročit zaplacenou částku

PoplatkyNikdy záporné a nikdy nad smluvními stropy

RezervyZůstatek po zpracování neklesne pod minimum

SlevyZůstávají v limitech i při kombinování slev

BodyVydané body nepřekročí rozpočtový limit

RozděleníRozdělené částky dávají dohromady původní jistinu

Balíček důkazů

Dodáváme znovu ověřitelné důkazy, ne odpověď AI.

FINITE FIELD

CERTIFIKÁT MPK

Kontrola připravenosti důkazu
Kanonický záznam certifikátu

VERDIKT JÁDRA
PŘIJATO

MPK

Hash certifikátu
Verdikt jádra MPK
Výsledek referenčního kontroleru Go
Zpráva o axiomech
Dokázané vlastnosti a uvedené předpoklady
Vyloučený rozsah a důvody mimo rozsah
Protipříklad, pokud byl nalezen
ID běhu a informace pro opětovnou kontrolu

Kontrola připravenosti důkazu

Zkontrolujte první funkci v pevném rozsahu.

198 000 JPY (bez daně)

Jedna funkce v Go
Až 2 vlastnosti k důkazu
Klasifikuje výsledky jako dokázané, protipříklad, neznámé nebo mimo rozsah
Balíček důkazů a online průchod výsledky

Zobrazit nabídku pro první nasazení

Toto je plánovaná standardní cena. Aktuálně běží kampaň pro první nasazení omezená na prvních 5 firem za 49 800 JPY bez daně.

Nabídka MPK pro první nasazení

Pouze pro prvních 5 firem

Ověřte, zda lze váš kritický kód v Go dokázat, nejen testovat.

V rámci kontroly připravenosti důkazu MPK vybereme jednu cílovou funkci v Go, definujeme vlastnost k zaručení, vygenerujeme kandidáty důkazu pomocí AI a spustíme nezávislou kontrolu jádrem MPK.

Co je zahrnuto

Jedna funkce v Go
Až 2 vlastnosti k důkazu
Posouzení kompatibility s MPK
Zpráva o důkazech, protipříkladech, překážkách důkazu a položkách mimo rozsah
Zpráva shrnující rozsah důkazu a předpoklady

Podmínky kampaně

Tato nabídka je určena firmám, které po službě poskytnou upřímnou zpětnou vazbu a schválí případovou studii ke zveřejnění na oficiálním webu MPK. Případová studie může obsahovat název firmy, jméno kontaktní osoby, pracovní pozici, zpětnou vazbu a reprezentativní fotografii nebo logo firmy.

Název firmyJménoPracovní poziceZpětná vazbaReprezentativní fotografie nebo logo firmy

Obsah před zveřejněním zkontrolujete a použijeme pouze schválené materiály. Nežádáme kladné hodnocení.

Průběh služby

Průběh služby (5 kroků)

Úvodní zjištění

Potvrdíme scénář selhání, který by mohl způsobit ztrátu, a cílovou funkci.

Uzamčení rozsahu

Uzamkneme funkci, vlastnost, předpoklady a vyloučený rozsah.

Kontrola Gemini + MPK

AI připraví kandidáty a MPK zkontroluje certifikát.

Průchod výsledky

Projdeme si důkaz, protipříklad, neznámý výsledek, vyloučení a důkazy.

Další kroky

Vyjasníme, zda pokračovat opravami, dalšími funkcemi nebo integrací CI/CD.

Nejvhodnější případy

Implementujete logiku refundací, poplatků nebo zůstatků v Go
Jediná chyba může způsobit finanční ztrátu nebo auditní zátěž
Nemáte vyhrazený tým pro formální verifikaci
Máte malou funkci, kterou lze izolovat od externího I/O

Současná omezení

Důkaz libovolné celé aplikace v Go
End-to-end zpracování zahrnující DB, API, síť nebo UI
Odhalení každé bezpečnostní zranitelnosti
Nepodporovaná syntaxe, externí závislosti nebo nejasné specifikace

FAQ

FAQ před první konzultací

Tyto odpovědi pokrývají běžné otázky před kontaktováním, včetně rozsahu důkazu, role AI a zacházení s kódem.

Odstraní to všechny chyby?

Ne. Zadanou vlastnost kontrolujeme pouze v rámci výslovných předpokladů, rozsahu a podporované podmnožiny Go. Nezaručuje to celou aplikaci ani externí systémy.

Musíme se učit Lean nebo Rocq?

Pro první kontrolu ne. Začínáme potvrzením funkce zásad v Go izolované od externího I/O a vlastnosti, kterou chcete zaručit.

Rozhoduje AI o tom, co je správně?

Ne. Gemini vytváří vlastnosti, důkazové strategie a kandidáty důkazu. Nezávislé jádro MPK konečný certifikát přijme nebo odmítne.

Co se stane, když důkaz selže?

Výsledek klasifikujeme jako protipříklad, neznámý nebo mimo rozsah a potom vysvětlíme důvod, potřebné specifikace, pravděpodobné opravy a způsob izolace dokazatelné jednotky.

Lze to integrovat do CI/CD?

Po potvrzení cíle a proveditelnosti důkazu v kontrole připravenosti důkazu můžeme samostatně navrhnout průběžné kontroly nebo integraci CI/CD.

Musíme s dotazem poslat kód?

Do veřejného formuláře nemusíte vkládat důvěrný kód. Po dotazu potvrdíme zacházení s NDA a bezpečný způsob sdílení.

Kontakt

Ověřte, zda lze váš kód dokázat.

Řekněte nám, které selhání by bylo nejzávažnější a kterou funkci v Go chcete zkontrolovat. Do veřejného formuláře nemusíte vkládat důvěrný kód.

Podporujeme NDA a bezpečné sdílení kódu

Název firmy

Jméno

Pracovní e-mail

Cílová logika

Které selhání by bylo nejzávažnější?

Požádat o NDA

Do veřejného formuláře nezadávejte zdrojový kód, přístupové údaje ani osobní údaje.

Náhled odeslání byl přijat. Na produkčním webu se napojí na stávající tok dotazů.