verification

5 posts

Кто-то действительно верифицировал 10 000 строк с нулевым количеством дефектов? IBM сделала это, и методология страннее результата.

Cleanroom software engineering обещала инкременты с нулевым количеством дефектов через mathematical verification вместо debugging. Мы смотрим на реальные данные проекта IBM, чтобы проверить, выдержал ли этот тезис.

Среднее значение по индустрии программного обеспечения в 1980-х годах составляло от 30 до 60 дефектов на тысячу строк кода. Команда Cleanroom в IBM поставила…

25 июля 2026 г.

model-checking autoverus rust verification

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 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 г.

n-version-programming equivalence-testing formal-methods verification

Тестирование не докажет, что две функции эквивалентны. Вот что докажет.

N-версионное программирование предполагает, что ваши реализации согласованы. Мы разбираем, почему тестов недостаточно, как SMT-солверы могут реально доказать эквивалентность и где провести границу между «достаточно хорошо» и формально верифицировано.

Вы построили n-версионную систему. Три независимые реализации одной и той же критической функции, voter, который выбирает результат большинства, и приятное…

14 июня 2026 г.