formal-methods

4 статьи

6 июл. 2026 г.

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

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

5 июл. 2026 г.

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

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

model-checking rust verification formal-methods

15 июн. 2026 г.

Differential testing работает без формального доказательства, но common-mode failures — вот подвох

Differential testing позволяет находить баги, не зная правильного ответа. Проблема в том, что коррелированные ошибки выглядят как согласие. Вот как обнаружить слепые зоны.

n-version-programming differential-testing formal-methods trust

14 июн. 2026 г.

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

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

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