MPK Assurance / Revue de préparation à la preuve Go
Nous vérifions mécaniquement la logique Go critique qui traite de l’argent, comme les remboursements, frais, soldes et réserves, à partir de spécifications, d’hypothèses et d’un périmètre explicites. Gemini prépare des candidats de preuve, puis le noyau MPK indépendant rend le verdict final.
Réservé aux 5 premières entreprises Offre de lancement MPK JPY 49,800(hors taxes)
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 viole la propriété.
Le noyau a accepté le certificat canonique corrigé.
Démo de remboursement en 30 secondes
Essayez le code de remboursement préparé et suivez le passage du contre-exemple à la correction, puis à une preuve réussie. Vous n’avez pas à saisir de code confidentiel dans la démo publique.
Règle de remboursement : les remboursements cumulés ne doivent pas dépasser le montant payé
Nous avons trouvé des entrées concrètes où le remboursement cumulé dépasse le montant payé.
Classification des résultats
La propriété spécifiée tient sous les hypothèses et le périmètre explicites.
PROUVÉNous montrons les entrées concrètes qui violent la propriété et clarifions la condition à corriger.
RÉFUTÉNous signalons clairement quand la stratégie actuelle ne permet pas de déterminer si la propriété tient.
INDÉTERMINÉNous expliquons les raisons précises qui empêchent de traiter la cible, comme une syntaxe non prise en charge, des E/S externes ou un comportement non pris en charge.
NON APPLICABLEDifférence avec les tests
| Comparaison | Tests | Preuve |
|---|---|---|
| Cible | Entrées sélectionnées | Propriété spécifiée |
| Affichage du contre-exemple | △ | ○ |
| Revérification | Journal d’exécution | Certificat |
| Jugement final | Suite de tests | Noyau |
Nous vérifions la propriété par rapport à des spécifications, des hypothèses et un périmètre explicites, pas seulement avec quelques exemples d’entrées.
Vous pouvez commencer par une fonction Go de règle métier critique, isolée des E/S externes.
L’IA ne fait que préparer des candidats. L’acceptation finale est effectuée par un noyau indépendant qui lit le certificat canonique.
Gemini exécute le flux de preuve, MPK prend la décision de confiance et un humain approuve la livraison.
Dossier de preuve
Revue de préparation à la preuve
Enregistrement canonique du certificat
Revue de préparation à la preuve
Il s’agit du tarif standard prévu. Nous menons actuellement une campagne de lancement réservée aux 5 premières entreprises, au prix de JPY 49,800 hors taxes.
Offre de lancement MPK
Réservé aux 5 premières entreprisesDans la revue de préparation à la preuve MPK, nous choisissons une fonction Go cible, définissons la propriété à garantir, générons des candidats de preuve avec l’IA, puis lançons une vérification indépendante avec le noyau MPK.
Cette offre s’adresse aux entreprises qui peuvent fournir un retour franc après la prestation et approuver la publication d’un cas client sur le site officiel de MPK. Ce cas peut inclure le nom de l’entreprise, le nom du contact, sa fonction, son retour, ainsi qu’une photo représentative ou le logo de l’entreprise.
Déroulement du service
Confirmer le scénario de défaillance pouvant causer une perte et la fonction cible.
Figer la fonction, la propriété, les hypothèses et le périmètre exclu.
L’IA prépare les candidats, et MPK vérifie le certificat.
Parcourir la preuve, le contre-exemple, le résultat indéterminé, les exclusions et les preuves fournies.
Clarifier s’il faut passer aux corrections, à d’autres fonctions ou à une intégration CI/CD.
FAQ
Ces réponses couvrent les questions fréquentes avant de nous contacter, notamment le périmètre de preuve, le rôle de l’IA et la gestion du code.
Non. Nous vérifions uniquement la propriété spécifiée, dans les hypothèses explicites, le périmètre et le sous-ensemble Go pris en charge. Cela ne garantit pas toute l’application ni les systèmes externes.
Pas pour la première revue. Nous commençons par confirmer une fonction Go de règle métier isolée des E/S externes et la propriété que vous voulez garantir.
Non. Gemini crée des propriétés, des stratégies et des candidats de preuve. Le noyau MPK indépendant accepte ou rejette le certificat final.
Nous classons le résultat comme contre-exemple, indéterminé ou hors périmètre, puis expliquons la raison, les spécifications nécessaires, les corrections probables et la manière d’isoler une unité prouvable.
Après confirmation de la cible et de la faisabilité de la preuve par la revue de préparation, nous pouvons proposer séparément des contrôles continus ou une intégration CI/CD.
Vous n’avez pas à coller de code confidentiel dans le formulaire public. Après votre demande, nous confirmerons la gestion de la NDA et une méthode de partage sécurisée.
Contact
Dites-nous quelle défaillance serait la plus critique et quelle fonction Go vous souhaitez faire examiner. Vous n’avez pas à coller de code confidentiel dans le formulaire public.
NDA et partage sécurisé du code pris en charge