@ilyasergey
Вышел Velvet 2.0, обновлённый на базе новейших механизмов верификации Lean. Версия стала проще в настройке и в 10 раз быстрее, получила спецификации исключений, ghost state, именованные цели доказательств и новые практические примеры — от алгоритма Дейкстры до ленивых деревьев отрезков. Также запущен новый сайт проекта.