Тэги: формальная верификация, zkVM, автоматное программирование, RISC-V, Lean
Cтатья Йоичи Хираи «Финальная форма разработки программного обеспечения». Автор — человек с десятилетним опытом в верификации программ, и статья написана серьёзно. Тезис: оптимальный путь к корректному ПО — писать ассемблерный код RISC-V и доказывать его корректность в системе Lean. Никакого Rust, C, C++. Только ассемблер и теоремы.
Я хочу разобрать, где этот тезис работает, где нет, и почему российская школа верификации программ задала правильный вопрос ещё тогда, когда никакого Lean не существовало.
Контекст: почему ассемблер
Автор работает над zkVM — виртуальными машинами, которые создают криптографическое доказательство того, что конкретная программа с конкретными входными данными дала конкретные выходные данные. Верификатор работает на уровне инструкций RISC-V. И здесь выбор ассемблера перестаёт казаться странным.
Цепочка такая: если между вашей логикой и машинным кодом стоит компилятор — вы не контролируете трансляцию. Даже у Rust нет формальной спецификации; смысл программы де-факто определяется поведением компилятора. Даже CompCert — формально верифицированный компилятор C — генерирует код на 20% медленнее, чем GCC -O3. Для zkVM, которая должна доказывать блоки Ethereum за секунды, это критично.
Вывод автора: раз LLM теперь умеют писать ассемблерный код, давайте уберём компилятор как источник неопределённости и работаем напрямую с тем, что верифицируется.
Логика безупречная. Для этой задачи.
Что именно доказывает Lean
Вот как выглядит спецификация 256-битного сложения в EVM из статьи:
cpsTriple base (base + 120) code
((.x12 ↦ᵣ sp) ** evmWordIs sp a ** evmWordIs (sp + 32) b)
((.x12 ↦ᵣ (sp + 32)) ** evmWordIs sp a ** evmWordIs (sp + 32) (a + b))
Это говорит: «после выполнения этого ассемблерного кода значение по адресу sp + 32 будет равно a + b». И Lean это доказывает.
Красиво. Но вот вопрос: а что такое a + b в контексте EVM?
Lean доказывает, что реализация соответствует спецификации. Он ничего не говорит о том, что спецификация соответствует задаче.
Два уровня корректности, которые легко перепутать
В теории верификации программ давно разделяют два понятия:
Verification — доказательство того, что программа соответствует формальной спецификации.
Validation — доказательство того, что спецификация соответствует реальной задаче.
Формальные методы — Lean, Rocq, Isabelle — закрывают первое. Второе остаётся вопросом к человеку, который писал спецификацию.
Это не академическая придирка. Это фундаментальное ограничение подхода. Если спецификация 256-битного сложения содержит ошибку — например, неверно обрабатывает overflow — Lean докажет, что ассемблерный код реализует это идеально точно.
Получается корректно доказанная ошибка: программа верифицирована, но неправильна. Дейкстра называл это «correct program, wrong problem» и считал одной из главных ловушек формальных методов.
Что сказал бы профессор Шалыто А.А.
Анатолий Шалыто в ИТМО разрабатывал подход, который в некотором смысле атакует эту проблему с другой стороны — через автоматное программирование.
Идея простая и сильная: корректность системы должна быть доказана до написания кода. Поведение описывается через конечные автоматы с явными состояниями и переходами. Эта модель верифицируется на уровне модели — model checking, формальные методы над графом состояний. Код генерируется из автомата, поэтому он корректен по построению.
Путь не «написал код → доказал», а «построил модель → верифицировал модель → сгенерировал код».
Шалыто задал бы Хираи один вопрос: откуда берётся корректность исходного кода? Ведь автор сам пишет: «Всё просто. Создайте корректный исходный код». Но это именно та часть, которая в статье вынесена за скобки.
Ирония в том, что оба подхода хотят одного — убрать человеческую ошибку из критического пути. Просто Шалыто начинает с модели, а Хираи заканчивает машинным кодом.
Критика тезиса «финальная форма»
Автор называет свой подход «финальным» в том числе в теоретико-категорийном смысле — как универсальный объект, к которому сводятся другие подходы.
Где тезис работает:
- zkVM и системы, где верификация происходит на уровне машинного кода
- Криптографические примитивы с жёсткими требованиями к производительности
- Контексты, где компилятор является частью модели угроз
Где тезис не работает:
Для большинства программного обеспечения задача верификации трансляции не стоит вообще. Там важно доказать корректность бизнес-логики. И здесь разрыв между спецификацией и реальностью — главная проблема, которую ассемблер + Lean не решают, а маскируют.
Кроме того, автор сам признаёт, что ИИ-агенты иногда допускают ошибки и «сами замечают их, когда проверка заходит в тупик». Но Lean проверяет только то, что написано в спецификации. Ошибка в спецификации в тупик не заводит — она проходит верификацию.
А что с типобезопасностью высокоуровневых языков?
Разумный вопрос: а можно ли верифицировать высокоуровневый код — скажем, с railway-oriented programming, машинами состояний, строгой типобезопасностью — без переписывания на ассемблер?
Да, но с условиями.
Railway-oriented programming и state machines — это паттерны, не формальные доказательства. Они снижают вероятность ошибки, но не дают математической гарантии.
Для верификации на уровне языка нужны языки с зависимыми типами или формальной операционной семантикой: Haskell + Liquid Haskell, F*, Idris, Agda. Там разрыв между «типы сходятся» и «программа корректна» минимален. Но всё равно остаётся проблема трансляции в машинный код — та, которую решает Хираи.
Подход через верифицированный компилятор (CompCert для C, CakeML для ML) закрывает этот разрыв формально, но ценой производительности — что в контексте zkVM неприемлемо.
Итог
Хираи решил конкретную инженерную задачу элегантно и обоснованно. Для zkVM его подход разумен. Но «финальная форма разработки ПО» — это громкое название для инструмента, который:
- Доказывает соответствие кода спецификации, но не корректность самой спецификации
- Оптимален для узкого класса задач с жёсткими требованиями к производительности и верификации на уровне байт
- Не отвечает на вопрос: как формально построить правильную модель до того, как начать писать код
Корректно доказанная ошибка остаётся ошибкой — очень хорошо документированной.