If you’re not already familiar with it, have a look at Dafny. It’s an imperative programming language built using Boogie and Z3 that allows extremely interestin

If you’re not already familiar with it, have a look at Dafny. It’s an imperative programming language built using Boogie and Z3 that allows extremely interesting compile time assertions.