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