Расскажите, пожалуйста, про Why3 (ну, в смысле, хотели бы вы его использовать в вашем идеальном проекте или нет)

Formalising the semantics of programming language is most of the time done using interactive proof assistants like Coq or Isabelle. Yet, formalising semantics and proving complex properties, with automatic provers only, was already shown possible by Clochard et. al, who also use the Why3 environment.