Have you looked at F* ? It's a Microsoft research language based on a subset of OCaml augmented with Z3 theorem prover: https://www.fstar-lang.org

Here's how the assertion of commutativity would look in F*:

  val f : int -> int -> Tot int
  let f a b = a + b
  let commutative = assert (forall a b. f a b = f b a )