MPK Assurance / Prüfung der Beweisbereitschaft für Go
Wir prüfen kritische Go-Logik, die Geld bewegt, etwa Rückerstattungen, Gebühren, Salden und Rücklagen, mechanisch gegen explizite Spezifikationen, Annahmen und einen festgelegten Umfang. Gemini bereitet Beweiskandidaten vor, und der unabhängige MPK-Kernel trifft die endgültige Entscheidung.
Auf die ersten 5 Unternehmen begrenzt MPK-Angebot für frühe Anwender JPY 49,800(zzgl. Steuer)
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 verletzt die Eigenschaft.
Der Kernel hat das korrigierte kanonische Zertifikat akzeptiert.
30-Sekunden-Demo zur Rückerstattung
Probieren Sie den vorbereiteten Rückerstattungscode aus und sehen Sie den Ablauf vom Gegenbeispiel über die Korrektur bis zum erfolgreichen Beweis. In der öffentlichen Demo müssen Sie keinen vertraulichen Code eingeben.
Rückerstattungsregel: Kumulierte Rückerstattungen dürfen den gezahlten Betrag nicht überschreiten
Wir haben konkrete Eingaben gefunden, bei denen die kumulierte Rückerstattung den gezahlten Betrag überschreitet.
Ergebnisklassifizierung
Die angegebene Eigenschaft gilt unter den expliziten Annahmen und im festgelegten Umfang.
BEWIESENWir zeigen konkrete Eingaben, die die Eigenschaft verletzen, und klären, welche Bedingung korrigiert werden muss.
WIDERLEGTWir berichten klar, wenn die aktuelle Strategie nicht bestimmen kann, ob die Eigenschaft gilt.
UNBEKANNTWir erläutern konkrete Gründe, warum das Ziel nicht bearbeitet werden kann, etwa nicht unterstützte Syntax, externe I/O oder nicht unterstütztes Verhalten.
NICHT ANWENDBARUnterschied zu Tests
| Vergleich | Tests | Beweis |
|---|---|---|
| Ziel | Ausgewählte Eingaben | Angegebene Eigenschaft |
| Anzeige von Gegenbeispielen | △ | ○ |
| Erneute Prüfung | Ausführungsprotokoll | Zertifikat |
| Endgültiges Urteil | Testsuite | Kernel |
Wir prüfen die Eigenschaft gegen explizite Spezifikationen, Annahmen und einen festgelegten Umfang, nicht nur gegen wenige Beispieleingaben.
Sie können mit einer kritischen Go-Richtlinienfunktion beginnen, die von externer I/O getrennt ist.
KI bereitet nur Kandidaten vor. Die endgültige Annahme erfolgt durch einen unabhängigen Kernel, der das kanonische Zertifikat liest.
Gemini führt den Beweisablauf aus, MPK trifft die Vertrauensentscheidung, und ein Mensch gibt die Lieferung frei.
Nachweispaket
Prüfung der Beweisbereitschaft
Kanonischer Zertifikatsdatensatz
Prüfung der Beweisbereitschaft
Dies ist der geplante Standardpreis. Derzeit läuft ein Angebot für frühe Anwender, begrenzt auf die ersten 5 Unternehmen, für JPY 49,800 zzgl. Steuer.
MPK-Angebot für frühe Anwender
Auf die ersten 5 Unternehmen begrenztIn der MPK-Prüfung der Beweisbereitschaft wählen wir eine Ziel-Go-Funktion aus, definieren die zu garantierende Eigenschaft, erzeugen Beweiskandidaten mit KI und führen eine unabhängige Prüfung mit dem MPK-Kernel aus.
Dieses Angebot richtet sich an Unternehmen, die nach der Leistung ehrliches Feedback geben und eine Fallstudie zur Veröffentlichung auf der offiziellen MPK-Seite freigeben können. Die Fallstudie kann Unternehmensname, Ansprechpartner, Position, Feedback sowie ein repräsentatives Foto oder Firmenlogo enthalten.
Leistungsablauf
Wir bestätigen das Fehlerszenario, das Verlust verursachen könnte, und die Zielfunktion.
Wir fixieren Funktion, Eigenschaft, Annahmen und ausgeschlossenen Umfang.
KI bereitet Kandidaten vor, und MPK prüft das Zertifikat.
Wir erläutern Beweis, Gegenbeispiel, unbekanntes Ergebnis, Ausschlüsse und Nachweise.
Wir klären, ob Korrekturen, weitere Funktionen oder CI/CD-Integration sinnvoll sind.
FAQ
Diese Antworten decken häufige Fragen vor der Kontaktaufnahme ab, darunter Beweisumfang, Rolle der KI und Umgang mit Code.
Nein. Wir prüfen nur die angegebene Eigenschaft innerhalb der expliziten Annahmen, des Umfangs und der unterstützten Go-Teilmenge. Das garantiert nicht die gesamte Anwendung oder externe Systeme.
Nicht für die erste Prüfung. Wir beginnen mit der Bestätigung einer von externer I/O getrennten Go-Richtlinienfunktion und der Eigenschaft, die Sie garantieren möchten.
Nein. Gemini erzeugt Eigenschaften, Beweisstrategien und Beweiskandidaten. Der unabhängige MPK-Kernel akzeptiert oder verwirft das endgültige Zertifikat.
Wir klassifizieren das Ergebnis als Gegenbeispiel, unbekannt oder außerhalb des Umfangs und erläutern danach Grund, erforderliche Spezifikationen, wahrscheinliche Korrekturen und die Abgrenzung einer beweisbaren Einheit.
Nachdem die Prüfung der Beweisbereitschaft Ziel und Beweisbarkeit bestätigt hat, können wir kontinuierliche Prüfungen oder CI/CD-Integration separat vorschlagen.
Sie müssen keinen vertraulichen Code in das öffentliche Formular einfügen. Nach der Anfrage klären wir NDA-Abwicklung und eine sichere Austauschmethode.
Kontakt
Teilen Sie uns mit, welcher Fehler am kritischsten wäre und welche Go-Funktion geprüft werden soll. Sie müssen keinen vertraulichen Code in das öffentliche Formular einfügen.
NDA und sichere Code-Freigabe werden unterstützt