Propiedad que se verifica
- Objetivo: una función de política de reembolsos
- Entradas: enteros no negativos
- E/S externa, base de datos y red quedan fuera del alcance
- Comprobado dentro de supuestos explícitos y un subconjunto de Go
MPK Assurance / Revisión de preparación para demostración en Go
Comprobamos mecánicamente lógica Go crítica que mueve dinero, como reembolsos, comisiones, saldos y reservas, frente a especificaciones, supuestos y alcances explícitos. Gemini prepara candidatos de demostración y el núcleo independiente de MPK emite el veredicto final.
Limitado a las primeras 5 empresas Oferta de adopción temprana de MPK 49.800 JPY(sin impuestos)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 incumple la propiedad.
El núcleo aceptó el certificado canónico corregido.
Demo de reembolsos de 30 segundos
Pruebe el código de reembolso preparado y vea el flujo desde el contraejemplo hasta la corrección y la demostración correcta. No necesita introducir código confidencial en la demo pública.
Política de reembolsos: los reembolsos acumulados no deben superar el importe pagado
Encontramos entradas concretas en las que el reembolso acumulado supera el importe pagado.
Clasificación de resultados
La propiedad especificada se cumple bajo los supuestos y el alcance explícitos.
DEMOSTRADOMostramos entradas concretas que incumplen la propiedad y aclaramos qué condición debe corregirse.
REFUTADOInformamos claramente cuando la estrategia actual no puede determinar si la propiedad se cumple.
INDETERMINADOExplicamos las razones concretas por las que no podemos tratar el objetivo, como sintaxis no compatible, E/S externa o comportamiento no compatible.
NO APLICABLEDiferencia frente a las pruebas
| Comparación | Pruebas | Demostración |
|---|---|---|
| Objetivo | Entradas seleccionadas | Propiedad especificada |
| Visualización de contraejemplo | △ | ○ |
| Reverificación | Registro de ejecución | Certificado |
| Juicio final | Suite de pruebas | Núcleo |
Comprobamos la propiedad frente a especificaciones, supuestos y alcance explícitos, no solo contra unas pocas entradas de ejemplo.
Puede empezar con una función crítica de reglas en Go, aislada de la E/S externa.
La IA solo prepara candidatos. La aceptación final la realiza un núcleo independiente que lee el certificado canónico.
Gemini ejecuta el flujo de demostración, MPK toma la decisión de confianza y una persona aprueba la entrega.
Paquete de evidencia
Revisión de preparación para demostración
Registro de certificado canónico
Revisión de preparación para demostración
Este es el precio estándar previsto. Actualmente ofrecemos una campaña de adopción temprana limitada a las primeras 5 empresas por 49.800 JPY sin impuestos.
Oferta de adopción temprana de MPK
Limitado a las primeras 5 empresasEn la revisión de preparación para demostración de MPK, elegimos una función Go objetivo, definimos la propiedad que se quiere garantizar, generamos candidatos de demostración con IA y ejecutamos una comprobación independiente con el núcleo de MPK.
Esta oferta está dirigida a empresas que puedan proporcionar comentarios sinceros después del servicio y aprobar un caso de estudio para su publicación en el sitio oficial de MPK. El caso de estudio puede incluir el nombre de la empresa, el nombre de contacto, el cargo, los comentarios y una fotografía representativa o el logotipo de la empresa.
Flujo del servicio
Confirmar el escenario de fallo que podría causar pérdidas y la función objetivo.
Fijar la función, la propiedad, los supuestos y el alcance excluido.
La IA prepara candidatos y MPK comprueba el certificado.
Repasar la demostración, el contraejemplo, el resultado indeterminado, las exclusiones y la evidencia.
Aclarar si conviene avanzar hacia correcciones, funciones adicionales o integración CI/CD.
FAQ
Estas respuestas cubren preguntas habituales antes de contactarnos, incluido el alcance de la demostración, el papel de la IA y el manejo del código.
No. Comprobamos la propiedad especificada solo dentro de los supuestos explícitos, el alcance y el subconjunto de Go compatible. Esto no garantiza toda la aplicación ni los sistemas externos.
No para la primera revisión. Empezamos confirmando una función de reglas en Go aislada de la E/S externa y la propiedad que quiere garantizar.
No. Gemini crea propiedades, estrategias y candidatos de demostración. El núcleo independiente de MPK acepta o rechaza el certificado final.
Clasificamos el resultado como contraejemplo, indeterminado o fuera de alcance, y después explicamos el motivo, las especificaciones necesarias, las correcciones probables y cómo aislar una unidad demostrable.
Después de que la revisión de preparación confirme el objetivo y la viabilidad de la demostración, podemos proponer por separado comprobaciones continuas o integración CI/CD.
No necesita pegar código confidencial en el formulario público. Tras la consulta, confirmaremos el manejo del NDA y un método seguro para compartirlo.
Contacto
Indíquenos qué fallo sería más importante y qué función Go quiere revisar. No necesita pegar código confidencial en el formulario público.
NDA y uso compartido seguro de código disponibles