I believe, Nim also has this functionality, although, it uses the [0]Z3Prover tool with a nim frontend [1]DrNim for proving.

[0]https://github.com/Z3Prover/z3

[1]https://nim-lang.github.io/Nim/drnim.html