Не нужно знать LTL, чтобы использовать model checker

Не нужно изучать линейную темпоральную логику, чтобы использовать model checker. Инструменты вроде Kani, CBMC и Alloy позволяют проверять свойства с помощью обычных assertions и реляционных constraints. Вы жертвуете возможностью доказывать свойства liveness ради кривой обучения, измеряемой часами вместо недель, и для большинства программных ошибок это обмен стоящий.

Temporal logic — это привратник, которого требуют большинство model checkers

Классические model checkers, SPIN и NuSMV, требуют выражать свойства в LTL или CTL. Вы пишете что-то вроде G(request -> F(response)), что означает «глобально, каждый запрос рано или поздно следует за ответом». Это мощно. Можно доказать, что ваш протокол никогда не попадает в deadlock, что каждое сообщение рано или поздно подтверждается, что ваша система fair.

Это также специализированный навык, которого нет у большинства практикующих разработчиков. Чтение формулы LTL — это не как чтение кода. Операторы модальны, семантика определена на бесконечных traces, и интуиция, выработанная при написании unit tests, не переносится. Поэтому вопрос справедлив: если вы хотите мощь поиска ошибок model checking, действительно ли нужно сначала покорить эту вершину?

Нет. Другой класс инструментов существует уже десятилетия, и он верифицирует код с помощью тех же assertions, что вы уже пишете.

Bounded model checkers превращают assertions в SAT-задачи

Bounded model checkers не требуют изучать новую логику. Они требуют написать test harness. Вы объявляете недетерминированные inputs, ограничиваете их assumptions и утверждаете свойства на языке хоста. Затем инструмент разворачивает циклы до заданной границы, кодирует программу как SAT- или SMT-формулу и просит solver найти counterexample.

Если solver возвращает UNSAT, ваше свойство выполняется для всех путей в пределах этой границы. Если найден counterexample, вы получаете конкретный trace, показывающий, какие именно inputs вызывают ошибку. Никаких темпоральных операторов. Никаких бесконечных traces. Просто нарушенный assertion с воспроизводимым вектором входных данных.

Kani — самый доступный bounded model checker для Rust. Устанавливается командой cargo install kani-verifier и работает на обычном Rust-коде.

Реальный пример: проверка state machine на Rust

Вот state machine с ошибкой. Она отслеживает простой counter, уменьшающийся на каждом tick до достижения нуля, после чего возвращается в состояние idle.

#[derive(Clone, Copy, PartialEq, Debug)]
enum State {
    Idle,
    Running,
    Stopped,
}

struct Machine {
    state: State,
    count: u32,
}

impl Machine {
    fn start(&mut self, initial: u32) {
        if self.state == State::Idle && initial > 0 {
            self.state = State::Running;
            self.count = initial;
        }
    }

    fn tick(&mut self) {
        if self.state == State::Running {
            self.count -= 1;
            if self.count == 0 {
                self.state = State::Idle;
            }
        }
    }

    fn stop(&mut self) {
        if self.state == State::Running {
            self.state = State::Stopped;
        }
    }
}

Ошибка тонкая. Посмотрите на stop. Он устанавливает состояние в Stopped, но оставляет count неизменным. Если позже что-то предполагает, что count == 0 при state == State::Stopped, это предположение неверно.

Вот Kani proof harness, который её ловит:

#[kani::proof]
fn check_stopped_implies_count_zero() {
    let mut machine = Machine {
        state: State::Idle,
        count: 0,
    };

    let initial: u32 = kani::any();
    kani::assume(initial > 0 && initial <= 10);

    machine.start(initial);
    machine.tick();
    machine.stop();

    assert!(
        machine.state != State::Stopped || machine.count == 0,
        "Stopped state should have count == 0"
    );
}

Kani исследует каждый path. Он находит, что при initial == 2 после start машина находится в состоянии Running с count == 2. Один tick уменьшает count до 1, но состояние остаётся Running. Затем stop устанавливает состояние в Stopped с count == 1. Assertion нарушается. Kani сообщает именно этот trace.

Это опыт model checking без temporal logic. Вы пишете на Rust. Вы пишете assertions на Rust. Инструмент говорит, какие inputs их нарушают.

Alloy находит ошибки уровня дизайна с помощью реляционной логики

Bounded model checkers верифицируют код. Alloy верифицирует дизайны.

Alloy — это model finder, а не традиционный model checker, но различие менее важно, чем workflow. Вы описываете систему как набор отношений, инварианты состояния как ограничения логики первого порядка и просите Alloy найти counterexample. Он ищет все возможные instances в рамках заданного пользователем scope и показывает диаграммы сбоя.

Вот модель Alloy для свойства простого ориентированного графа:

sig Node {
    next: set Node
}

pred reachable[n1, n2: Node] {
    n2 in n1.^next
}

assert symmetric_reachability {
    all n1, n2: Node |
        reachable[n1, n2] implies reachable[n2, n1]
}

check symmetric_reachability for 3

Assertion утверждает, что reachability симметрична. Alloy проверяет это для всех графов с не более чем тремя узлами и сразу рисует counterexample: граф, в котором n1 указывает на n2, но у n2 нет исходящих рёбер. Операторы G, F или U нигде не появляются.

Что вы жертвуете: liveness и бесконечное поведение

Это удобство имеет цену. Bounded model checkers проверяют поведение только до границы цикла или длины trace. Они не могут доказать, что запрос рано или поздно получит ответ, только что за первые N шагов ничего плохого не произойдёт. Alloy проверяет только instances в рамках своего scope. Он не может доказывать свойства для сколь угодно больших систем, только что под границей не существует counterexample.

Если нужно доказать, что ваш протокол консенсуса никогда не теряет зафиксированные записи, или что каждое сообщение рано или поздно доставляется, вам всё ещё нужны temporal logic и unbounded model checking. Инструменты вроде TLA+ заворачивают temporal logic в синтаксис, похожий на обычную математику, а не модальную логику, но лежащая в основе семантика остаётся темпоральной.

Для инвариантов структур данных, enforcement контрактов API и поиска race condition, которая срабатывает только на 47-м пути выполнения, bounded-инструментов обычно достаточно. Они ловят ошибки, которые пропускают unit tests, и делают это с помощью assertions, которые можно прочитать без учебника.

Начало работы с Kani за пять минут

Если у вас установлен Rust, bounded model checking находится на расстоянии одной команды.

cargo install kani-verifier
cargo kani setup

Создайте новый crate, напишите функцию с тонкой ошибкой и добавьте harness #[kani::proof]. Запустите cargo kani. Если Kani находит counterexample, он выводит конкретные inputs, вызывающие сбой. Если сообщает VERIFICATION SUCCESSFUL, ваше свойство выполняется для всех путей в пределах стандартных границ.

Начните с функций, у которых небольшие пространства состояний и чёткие инварианты. State machines, валидация парсеров и переходы состояний протоколов — идеальные первые цели. Не пытайтесь верифицировать целый HTTP-сервер с первого раза. У SAT solver есть пределы, и у вашего терпения тоже.

FAQ: bounded и unbounded, liveness и с чего начать

Является ли bounded model checking настоящим model checking?

Технически это вариант, кодирующий задачу как satisfiability query, а не явно исследующий state graph. Для разработчика, пытающегося найти ошибки, разница академическая. Он систематически исследует все пути, что и означает model checking на практике.

Можно ли доказать liveness с помощью Kani или CBMC?

Нет напрямую. Свойства liveness требуют рассуждений о бесконечном поведении, а bounded-инструменты явно ограничивают поиск. Иногда можно закодировать bounded-проверку liveness, развернув достаточно шагов для достижения fixpoint, но это продвинутая техника.

А как насчёт TLA+? Требует ли он temporal logic?

TLA+ использует Temporal Logic of Actions, так что технически да. Но Лесли Лампорт спроектировал синтаксис так, чтобы он читался как обычная математика. Большинство спецификаций TLA+ тратят 90% текста на инварианты состояния и ограничения структур данных, а не на темпоральные операторы. Это самый доступный путь, если вам нужен unbounded temporal reasoning.

Стоит ли использовать Alloy или Kani?

Используйте Kani, если у вас есть Rust-код и вы хотите верифицировать детали реализации. Используйте Alloy, если вы ещё проектируете систему и хотите исследовать, возможны ли ваши инварианты, прежде чем писать код.

Выбирайте инструмент, соответствующий вашей задаче, а не амбициям

Temporal logic прекрасна и мощна, но она не является необходимым условием для формальной верификации. Bounded model checkers и реляционные model finders позволяют выражать свойства на языках, которые вы уже знаете. Они не докажут, что ваша система рано или поздно завершится, но найдут ошибку off-by-one, которая повреждает вашу state machine базы данных. Для большинства команд это та ошибка, которая имеет значение.

Начните с Kani на одной функции с состоянием. Напишите один assertion. Позвольте solver сказать, что вы упустили.