https://github.com/pschanely/CrossHair SMT solver + function contract annotations + generative testing = automated counterexample search. Would be interesting to use spec or Typed Clojure for a similar purpose.