🦀 Как доказать, что Rust-код работает правильно: Amazon рассказывает о Verus

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

Разработчик описывает прямо в исходниках:

* requires - условия перед выполнением функции.
* ensures — свойства результата.
* Инварианты циклов и вспомогательные доказательства.

Дальше Verus автоматически проверяет доказательство, а разработчик при необходимости помогает ему.

В статье есть показательный пример с бинарным поиском. Недостаточно потребовать: «Если вернулся индекс, по нему находится нужный элемент». Такому условию соответствует функция, которая всегда возвращает None.

Нужно добавить второе требование: если вернулся `None`, искомого элемента действительно нет в массиве.

Amazon уже использует Verus для проверки ключевых примитивов Nitro Isolation Engine, отвечающего за изоляцию виртуальных машин. Инструмент также позволяет доказывать свойства конкурентного кода и безопасность поддерживаемых конструкций unsafe.

Гарантии относятся к заданной спецификации и принятым допущениям: полнота самих требований остаётся ответственностью разработчика.

📖 https://www.amazon.science/blog/developing-provably-correct-rust-code-with-verus

#Rust #Разработка #FormalVerification