Smart Contracts can be written in DeepSEA, a functional programming language built to formally verify proofs through the Coq proof assistant. Backed with grants from the IBM and Ethereum Foundation, DeepSEA can be accessed through the CLI or DeepWallet. The DeepSEA compiler has a verified backend that generates EVM-compatible bytecode. This allows us to be sure that the generated Coq code actually represents what the EVM bytecode is doing.

Resources on DeepSEA