Autotomy — Expo Starter Pack
Русский
Ваш аккаунт

model-checking

6 статей

Назад ко всем статьям

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

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

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

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

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

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

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

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

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

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