model-checking

6 posts

AutoVerus превращает 40 часов написания proof в 3 вызова LLM. Хитрость в том, чтобы знать, когда сдаваться.

AutoVerus использует сеть агентов LLM для генерации proof корректности Verus для кода на Rust, автоматизируя более 90% proof obligations через цикл generate-repair-discharge, управляемый обратной связью SMT-solver.

Самая сложная часть формальной верификации никогда не заключалась в verifier. Она заключается в написании proof. Дайте опытному инженеру по Rust Verus —…

9 июля 2026 г.

model-checking llm rust formal-proofs

LLM могут генерировать код на Rust. Формальные доказательства — это совершенно другая проблема.

Большие языковые модели пишут удивительно хороший код на Rust, но когда вы просите их о формальном доказательстве, они галлюцинируют инварианты и изобретают синтаксис, который не принимает ни один верификатор. Вот что они на самом деле делают правильно, где ломаются и как их всё равно использовать.

LLM могут писать Rust, который компилируется и даже проходит . Что они не могут делать надёжно — так это писать формальное доказательство того, что код…

8 июля 2026 г.

model-checking race-conditions concurrency testing

Ожидание race conditions — ужасная стратегия тестирования

Почему model checking превосходит дни продакшен-рантайма в поиске concurrency-багов и как применить его к собственному коду.

Ждать, пока race conditions проявятся в продакшене, — это не тестирование. Это надежда, замаскированная под добросовестность. Вы можете запускать приложение…

7 июля 2026 г.

model-checking temporal-logic formal-methods verification

Можно верифицировать код с помощью model checking, не изучая temporal logic

Bounded model checkers вроде Kani и реляционные model finders вроде Alloy позволяют проверять свойства с помощью обычных assertions и constraints. Вы жертвуете доказательствами liveness ради кривой обучения, измеряемой часами, а не неделями.

Не нужно изучать линейную темпоральную логику, чтобы использовать model checker. Инструменты вроде Kani, CBMC и Alloy позволяют проверять свойства с помощью…

6 июля 2026 г.

model-checking rust verification formal-methods

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

Инструменты model checking вроде Kani позволяют верифицировать свойства Rust с помощью assertions вместо формальных доказательств. Проблема в том, что происходит, когда ваши циклы не имеют маленьких границ.

Можно доказать корректность кода на Rust, не написав ни одного доказательства. Инструмент, который это делает, называется model checker, а для Rust наиболее…

5 июля 2026 г.

model-checking distributed-systems tlaplus protocol-design

Распределённый протокол нельзя покрыть юнит-тестами, но можно проверить модельно

Исправление распределённых багов после деплоя обходится дорого. Модельная проверка позволяет найти их до написания хотя бы одной строчки кода реализации. Вот как это сделать с помощью TLA+.

Распределённый протокол нельзя покрыть юнит-тестами. Юнит-тест запускает один процесс на одной машине в одном порядке. Ваш протокол запускает десять процессов…

4 июля 2026 г.