Автор прогнал агентов по реализации Zstd на Rust с 26 вариантами промптов: от «делай TDD», Lean 4 и QuickCheck до SMT-солверов, TLA+ и «не ошибайся». Он заранее зарегистрировал прогнозы: TDD, скорее всего, просядет, формальные методы не обойдут хорошие тест-техники, а «Make no mistakes» с вероятностью 95% не сработает. Результаты в доступном фрагменте пока не разобраны.
Microsoft Research и Inria развивают F* — proof-oriented язык с зависимыми типами и SMT-решателями. Компилируется в OCaml, C и Wasm. Код на F* используется в Firefox, Linux, Azure Hyper-V для верифицированной криптографии (HACL*, EverCrypt) и парсинга сетевых пакетов (EverParse).
LWN разбирает, как BPF verifier пытается статически анализировать циклы и почему это до сих пор боль. Раньше он прогонял итерации почти поштучно и мог упереться в лимит, а теперь разработчики подтягивают special support и scalar evolution, чтобы не превращать проверку в бесконечный калькулятор для простого `for`.
Creusot — это инструмент для формальной проверки Rust-кода, то есть для тех случаев, когда «ну вроде работает» уже не считается аргументом. Проект живет на GitHub и явно рассчитан на людей, которым мало borrow checker'а и хочется ещё и математически доказать, что они не сломали инварианты.