MPK Assurance / проверка готовности доказательства для Go
Мы механически проверяем критически важную логику Go, которая управляет деньгами, например возвратами, комиссиями, балансами и резервами, относительно явно заданных спецификаций, предположений и границ проверки. Gemini готовит варианты доказательства, а независимое ядро MPK выносит окончательное решение.
Только для первых 5 компаний Предложение для раннего внедрения MPK 49 800 иен(без учета налога)
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 нарушает свойство.
Ядро приняло исправленный канонический сертификат.
30-секундное демо возврата
Попробуйте подготовленный код возврата и посмотрите путь от контрпримера к исправлению и успешному доказательству. В публичном демо не нужно вводить конфиденциальный код.
Политика возвратов: суммарные возвраты не должны превышать оплаченную сумму
Мы нашли конкретные входные данные, при которых суммарный возврат превышает оплаченную сумму.
Классификация результатов
Заданное свойство выполняется при явно указанных предположениях и границах проверки.
ДОКАЗАНОМы показываем конкретные входные данные, нарушающие свойство, и уточняем, какое условие нужно исправить.
ОПРОВЕРГНУТОМы ясно сообщаем, когда текущая стратегия не может определить, выполняется ли свойство.
НЕИЗВЕСТНОМы объясняем конкретные причины, по которым цель нельзя обработать: неподдерживаемый синтаксис, внешний ввод-вывод или неподдерживаемое поведение.
НЕПРИМЕНИМООтличие от тестирования
| Сравнение | Тестирование | Доказательство |
|---|---|---|
| Цель | Выбранные входные данные | Заданное свойство |
| Показ контрпримера | △ | ○ |
| Повторная проверка | Журнал выполнения | Сертификат |
| Окончательное решение | Набор тестов | Ядро |
Мы проверяем свойство относительно явных спецификаций, предположений и области проверки, а не только на нескольких примерах.
Можно начать с критически важной функции бизнес-правил на Go, изолированной от внешнего ввода-вывода.
ИИ только готовит варианты. Окончательное принятие выполняет независимое ядро, которое читает канонический сертификат.
Gemini выполняет процесс доказательства, MPK принимает решение о доверии, а человек утверждает результат передачи.
Пакет доказательных материалов
Каноническая запись
сертификата проверки готовности доказательства
Проверка готовности доказательства
Это плановая стандартная цена. Сейчас действует кампания раннего внедрения для первых 5 компаний: 49 800 иен без учета налога.
Предложение для раннего внедрения MPK
Только для первых 5 компанийВ проверке готовности доказательства MPK мы выбираем одну целевую функцию Go, определяем свойство, которое нужно гарантировать, генерируем варианты доказательства с помощью ИИ и выполняем независимую проверку ядром MPK.
Это предложение предназначено для компаний, которые могут дать откровенную обратную связь после услуги и согласовать кейс для публикации на официальном сайте MPK. Кейс может включать название компании, имя контактного лица, должность, отзыв, а также представительскую фотографию или логотип компании.
Процесс услуги
Подтверждаем сценарий сбоя, который может привести к потерям, и целевую функцию.
Фиксируем функцию, свойство, предположения и исключенную область.
ИИ готовит варианты, а MPK проверяет сертификат.
Разбираем доказательство, контрпример, неизвестный результат, исключения и доказательные материалы.
Уточняем, переходить ли к исправлениям, дополнительным функциям или интеграции с CI/CD.
FAQ
Здесь собраны ответы на частые вопросы перед обращением: область доказательства, роль ИИ и обработка кода.
Нет. Мы проверяем только заданное свойство в рамках явных предположений, области проверки и поддерживаемого подмножества Go. Это не дает гарантии для всего приложения или внешних систем.
Для первой проверки — нет. Мы начинаем с подтверждения функции бизнес-правил на Go, изолированной от внешнего ввода-вывода, и свойства, которое вы хотите гарантировать.
Нет. Gemini создает свойства, стратегии и варианты доказательства. Независимое ядро MPK принимает или отклоняет финальный сертификат.
Мы классифицируем результат как контрпример, неизвестный или вне области проверки, затем объясняем причину, необходимые спецификации, вероятные исправления и способ выделить доказуемый модуль.
После того как проверка готовности доказательства подтвердит цель и реализуемость доказательства, мы отдельно предложим непрерывные проверки или интеграцию с CI/CD.
Не нужно вставлять конфиденциальный код в публичную форму. После обращения мы согласуем работу по NDA и безопасный способ передачи.
Контакт
Расскажите, какой сбой был бы наиболее критичным и какую функцию Go нужно проверить. Конфиденциальный код не нужно вставлять в публичную форму.
Поддерживаем NDA и безопасную передачу кода