VerifyThis это серия соревнования по верификации программ, которые проходят ежегодно с 2011 года. Сейчас проходит отбор задач для соревнования этого года, которое пройдет в рамках конференции ETAPS 6 и 7 апреля в Люксембурге. Как я понял нет никакого ограничения по инструментам для верификации и команда сама выбирает наиболее удобный, за прошлые года на сайте указаны инструменты, которые использовали победившие команды: Why3, mCRL2, Dafny, VeriFast. На скриншоте типичная задача с соревнования.