Clojure Spec is a contract system, which is a common way to write code specifications. You can formally verify it in theory; ACL2, another lisp, is used in formal verification. It's also hard to compose formally-verified code, as Lars talks about in the original link.
Thanks for the correction. I've wanted to see more examples of Clojure Spec in practice because I had really understood it as an interface description language.
