Not formal verification, but you can specify and validate application state of SPAs written in clojurescript using clojure.spec(https://clojure.org/about/spec).

Example -- (https://github.com/Day8/re-frame/blob/master/examples/todomv...)

You might wanna check out ACL2, which is a theorem prover rooted in common lisp: http://www.cs.utexas.edu/users/moore/acl2/