Binary package “dafny” in ubuntu bionic

programming language with program correctness verifier

 Dafny is a programming language with a program verifier. The verifier
 processes function preconditions, postconditions, and assertions, and sends
 them to an SMT solver for checking. In this way, assertion failures become
 compiler errors, rather than runtime ones.