Можно доказать корректность кода на Rust, не написав ни одного доказательства, но пространство состояний — это плата

Можно доказать корректность кода на Rust, не написав ни одного доказательства. Инструмент, который это делает, называется model checker, а для Rust наиболее практичным на данный момент является Kani, созданный AWS. Вы пишете обычные assertions на Rust. Kani превращает их в математические утверждения и проверяет для каждого возможного входа. Никаких theorem provers. Никаких proof assistants. Никаких полугодовых отвлечений на Coq.

Подвох в том, что “каждый возможный вход” работает только когда пространство входов достаточно мало для исчерпывающего перебора. Если ваша функция принимает Vec<u8> с миллионом элементов, Kani не будет проверять каждую перестановку. Он проверит до заданной вами границы или будет работать, пока у ноутбука не кончится RAM. Доказательство реально, но оно ограничено.

Что на самом деле означает “доказательство без доказательств”

Формальная верификация обычно означает написание программы в proof assistant вроде Coq, ручное определение инвариантов и тактическое ведение solver. На верифицированный компилятор вроде CompCert ушли годы. У большинства команд нет лет.

Model checking — это другое. Вы пишете обычный Rust. Добавляете тестовую функцию с аннотацией #[kani::proof]. Внутри создаёте символьные значения с помощью kani::any(), вызываете свой код и делаете assertions. Kani компилирует ваш код в логическую формулу и передаёт её SMT solver. Solver либо подтверждает, что свойство выполняется для всех входов в пределах границы, либо выдаёт конкретный контрпример.

Вы не написали доказательство. Вы написали тест с универсальным квантором. Доказательство написал инструмент.

Как Kani превращает Rust в логику

Kani — это bounded model checker. Он разворачивает ваш код в логическую формулу и спрашивает SMT solver, может ли какой-либо путь выполнения нарушить assertion. Solver трактует переменные как символьные. Обычный тест даёт x значение 5. Доказательство Kani даёт x символ, представляющий каждое возможное значение u32.

Вот тривиальный пример. У нас есть функция, которая никогда не должна переполняться, и мы хотим это доказать.

// src/lib.rs
pub fn saturating_double(x: u32) -> u32 {
    x.saturating_mul(2)
}

#[cfg(kani)]
mod proofs {
    use super::*;

    #[kani::proof]
    fn check_saturating_double_never_overflows() {
        let x: u32 = kani::any();
        let result = saturating_double(x);
        if x > u32::MAX / 2 {
            assert_eq!(result, u32::MAX);
        } else {
            assert_eq!(result, x * 2);
        }
    }
}

Запустите cargo kani, и Kani верифицирует это за секунды. Он проверяет все 4 294 967 296 возможных значений x, не выполняя их по одному. SMT solver рассуждает о символьном представлении и заключает, что контрпримера не существует.

Guard #[cfg(kani)] означает, что этот код компилируется только под Kani. Он не раздувает ваш release build.

Реальный пример: доказать, что парсер не падает

Переполнения — это просто. Интересные случаи зависят от данных. Допустим, у нас есть функция, которая разбирает небольшой заголовок протокола. Мы хотим доказать, что она никогда не паникует, какие бы байты мы ей ни подали.

// src/protocol.rs
#[derive(Debug, PartialEq)]
pub enum ParseError {
    TooShort,
    InvalidVersion,
}

pub struct Header {
    pub version: u8,
    pub length: u16,
}

/// Parse a 4-byte header:
/// - byte 0: version (must be 1)
/// - byte 1: reserved (ignored)
/// - bytes 2-3: length in big-endian
pub fn parse_header(buf: &[u8]) -> Result<Header, ParseError> {
    if buf.len() < 4 {
        return Err(ParseError::TooShort);
    }
    let version = buf[0];
    if version != 1 {
        return Err(ParseError::InvalidVersion);
    }
    let length = u16::from_be_bytes([buf[2], buf[3]]);
    Ok(Header { version, length })
}

#[cfg(kani)]
mod proofs {
    use super::*;

    #[kani::proof]
    #[kani::unwind(5)]
    fn check_parse_header_no_panic() {
        let len: usize = kani::any();
        kani::assume(len <= 8);
        let buf: [u8; 8] = kani::any();
        let _ = parse_header(&buf[..len]);
    }
}

Kani верифицирует, что parse_header никогда не паникует для любого входного буфера длины от 0 до 8. Он проверяет bounds test, проверку версии и индексацию массива. Если бы мы написали buf[1] вместо того чтобы сначала проверить длину, Kani нашёл бы контрпример: 1-байтовый буфер, в котором buf[1] выходит за границы.

Аннотация #[kani::unwind(5)] говорит Kani, сколько раз разворачивать циклы. Поскольку в нашей функции нет циклов, это консервативно.

Проблема ограничения: где model checker упирается в стену

Model checking является исчерпывающим в пределах своих границ. За пределами этих границ он ничего не говорит. Это фундаментальный компромисс.

Циклы — первая стена. Kani должен развернуть каждый цикл фиксированное число раз. Если ваша функция итерирует Vec и вы задаёте границу unwind в 10, Kani доказывает корректность для векторов длины от 0 до 10. Он ничего не говорит о длине 11. Каждое увеличение умножает пространство состояний. Unwind в 50 может закончиться за минуты. Unwind в 500 может не закончиться никогда.

Рекурсия аналогична. Каждый вызов расширяет формулу. Глубокая рекурсия взрывает потребление памяти.

Размер данных — вторая стена. Kani хорошо справляется с массивами фиксированного размера. С динамически выделяемыми коллекциями у него проблемы, если явно не ограничить их размер.

Стандартная библиотека — третья стена. Kani моделирует многое из неё, но не всё. Если вы вызываете что-то, чего Kani не понимает, доказательство падает с ошибкой об отсутствии определения функции.

Что Kani может доказать и где он не справляется

Kani хорошо находит panics, переполнения целых чисел и нарушения assertions в ограниченном коде. Он отлично подходит для криптографических примитивов, парсеров протоколов и небольших state machines. Это места, где один неправильный вход вызывает катастрофу, а код естественно ограничен.

Kani плохо справляется с доказательством свойств liveness, вроде “каждый запрос в конце концов получает ответ”. Это требует рассуждений о бесконечных выполнениях, чего bounded model checking явно не делает. Для liveness нужен temporal model checker вроде TLA+.

Kani также не заменяет тесты. Пройденное доказательство говорит, что в пределах границы нет контрпримера. Тест говорит, что код ведёт себя корректно для конкретного входа, который вам важен. Kani ловит краевые случаи, о которых вы не подумали. Тесты ловят проблемы интеграции, которые Kani не видит.

Запуск Kani в CI без расплавления раннеров

Одно доказательство Kani для маленькой функции занимает секунды. Сьют для реальной crate занимает минуты. Доказательство с высокими границами unwind может занимать часы. Вы не хотите, чтобы ваша CI-пайплайн ждал двухчасового SMT-решения.

Держите доказательства Kani маленькими и быстрыми. Доказывайте safety-critical функции, те, где баг — это инцидент. Не пытайтесь доказать весь ваш web framework. Задайте timeout, может, пять минут на доказательство, и трактуйте timeout как failure to prove, а не как proof of failure.

Вот шаблон Makefile, который работает:

# Makefile
kani:
	cargo kani --only-codegen --output-format=terse
	cargo kani --timeout 300 --all-functions --enable-unstable

kani-fast:
	cargo kani --only-codegen --output-format=terse
	cargo kani --timeout 60 --all-functions --enable-unstable

kani-fast запускается в CI на каждый pull request. kani запускается ночью. Если доказательство регрессирует, вы узнаете в течение дня, а не после релиза.

Если вы экспортируете публичное API, напишите одно доказательство Kani на каждую публичную функцию, которая вызывает его с полностью символьными входами. Это максимально близко к formal contract test. Оно не доказывает, что реализация корректна, но доказывает, что реализация не падает на произвольных валидных входах.

Когда стоит обратиться к настоящему proof assistant

Если вам нужно доказывать свойства о неограниченных структурах данных, вроде “этот связный список всегда ацикличен”, Kani вам не поможет. Граница unwind сводит утверждение на нет. Для этого нужен инструмент вроде Creusot, который транслирует Rust в WhyML и использует proof assistant. Это больше работы, но он справляется с неограниченными структурами.

Если нужны доказательства эквивалентности или детекция undefined behavior, инструменты вроде MIRI или KLEE находятся в разных точках спектра effort-versus-coverage. Kani — это sweet spot для “у меня ограниченный код, и я хочу знать, паникует ли он”. Парсеры, декодеры, сериализаторы и валидаторы конфигурации — все подходят. Система типов Rust уже устраняет целые классы багов. Kani устраняет те, которые система типов достичь не может.

С чего начать

Если у вас есть Rust-crate с функцией, которая вас пугает, добавьте Kani. Пугающая функция обычно та, что разбирает untrusted input, делает битовые манипуляции или индексирует массивы. Напишите proof harness, который вызывает её с kani::any(). Запустите cargo kani. Если проходит — у вас есть ограниченное доказательство отсутствия падений. Если падает — у вас есть конкретный контрпример, который стал бы баг-репортом.

Вам не нужно учить новый язык. Вам не нужно понимать секвенциальное исчисление. Вы пишете assertions на Rust, и solver говорит, выполняются ли они. Это не формальное доказательство в академическом смысле. Это механическое доказательство в практическом смысле, а для большинства ПО практичное — это именно то, что нужно.

---

Часто задаваемые вопросы

Что такое model checking в верификации ПО?

Model checking — это автоматизированная техника, которая исчерпывающе исследует все возможные состояния системы, чтобы верифицировать, выполняются ли заданные свойства. Для Rust инструменты вроде Kani используют bounded model checking, чтобы доказывать assertions для всех возможных входов в пределах заданных границ, без необходимости ручного построения доказательств.

Чем Kani отличается от написания unit tests?

Unit test проверяет один конкретный вход. Доказательство Kani проверяет каждый вход в пределах границы. Если доказательство Kani проходит, вы знаете, что в ограниченном пространстве состояний нет контрпримера. Доказательство сильнее, но ограничено заданными вами границами.

Может ли Kani доказать, что всё моё Rust-приложение корректно?

Нет. Kani лучше всего работает на маленьких, ограниченных функциях. Пространство состояний растёт экспоненциально с итерациями циклов, глубиной рекурсии и размером данных. Используйте Kani для safety-critical компонентов вроде парсеров и обработчиков протоколов, а не для прикладной логики.

Что происходит, когда Kani встречает цикл без фиксированной границы?

Kani требует границу unwind для циклов. Если цикл может выполниться больше раз, чем позволяет граница, Kani вставляет unwinding assertion, которая падает. Вам нужно либо поднять границу, либо отрефакторить код так, чтобы количество итераций было известно статически. Это главное ограничение bounded model checking.