@ilyasergey
Илья Сергей представил Vermilion — экспериментальный бэкенд на Lean 4 для верификатора Verus для Rust, созданный за два уикенда. Условия верификации оформляются как читаемые теоремы Lean, которые можно доказывать с помощью SMT-решателя, Lean grind, лемм Mathlib, вручную или с использованием ИИ-систем.