9 posts
AutoVerus использует сеть агентов LLM для генерации proof корректности Verus для кода на Rust, автоматизируя более 90% proof obligations через цикл generate-repair-discharge, управляемый обратной связью SMT-solver.
Самая сложная часть формальной верификации никогда не заключалась в verifier. Она заключается в написании proof. Дайте опытному инженеру по Rust Verus —…
Большие языковые модели пишут удивительно хороший код на Rust, но когда вы просите их о формальном доказательстве, они галлюцинируют инварианты и изобретают синтаксис, который не принимает ни один верификатор. Вот что они на самом деле делают правильно, где ломаются и как их всё равно использовать.
LLM могут писать Rust, который компилируется и даже проходит . Что они не могут делать надёжно — так это писать формальное доказательство того, что код…
Инструменты model checking вроде Kani позволяют верифицировать свойства Rust с помощью assertions вместо формальных доказательств. Проблема в том, что происходит, когда ваши циклы не имеют маленьких границ.
Можно доказать корректность кода на Rust, не написав ни одного доказательства. Инструмент, который это делает, называется model checker, а для Rust наиболее…
Стандартная библиотека Rust предоставляет окружающее файловое полномочие каждой зависимости. cap-std заменяет его API на основе полномочий, которые заставляют код доказывать, что у него есть право доступа к пути, прежде чем он откроет его.
Любой crate в дереве ваших зависимостей может открыть , записать в ваш каталог или перечислить каждый файл в вашем проекте. Стандартная библиотека Rust не…
Выброшенные исключения скрывают пути отказа от вашей системы типов. Вот почему явный возврат ошибок делает ваш код более честным, и как перейти на него, не ненавидя свою жизнь.
Сигнатура вашей функции говорит, что она возвращает . Это не так. Она возвращает или взрывается. Система типов просто не знает о второй ветке. Это…
Однополевая обёрточная структура ловит баги смешения единиц измерения и путаницу типов, не добавляя ни одного байта накладных расходов.
Передайте с идентификатором пользователя в функцию, которая ожидает идентификатор заказа, и Rust не пожалуется. Оба типа — . Компилятор видит одинаковые типы,…
cargo-mutants находит тесты, которые только притворяются, что проверяют ваш код. Вот как работает mutation testing в Rust, что он ловит и стоит ли затрат времени компиляции.
У вас 100% покрытие строк. Каждая ветвь задействована. Каждая функция вызвана. Затем кто-то меняет на в вашей логике ценообразования, запускает тесты, и все…
Тестирование на примерах покрывает только те входные данные, о которых вы подумали. Тестирование на основе свойств генерирует случайные данные, проверяет инварианты и сокращает ошибки до минимальных контрпримеров.
Вы написали функцию . Вы протестировали её с и . Тест проходит. Вы выкатываете в продакшн. Пользователь передаёт срез из одного элемента. Ваша функция теряет…
Rust автоматически удаляет debug assertions, но настоящий design-by-contract требует большего, чем debug_assert!. Вот как построить zero-cost runtime contracts, которые исчезают из вашего релизного бинарника.
Rust может enforce runtime contracts в development и полностью стирать их из релизных сборок. Оговорка в том, что язык не рассматривает contracts как…