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...)