There's also Simplicity, which is not Turing complete and includes formal verification with Coq https://news.ycombinator.com/item?id=15588380

How about http://statebox.org?

Pact (http://github.com/kadena-io/pact) is a turing-incomplete LISP (no recursion, no lambdas, no unbounded loops ... no macros either ;) ) and built in Haskell. Also has formal verification by directly compiling to SMT-LIB2 (not released yet, but watch a demo! https://youtu.be/l7XuSuEe-Yg?t=22m23s).