I’m involved in smart-contracts security for ~8 years now (since the DAO hack). Have been an auditor, a CTO of an auditing organization and a hacker.
I’m very skeptical about formal verification. It is not possible to “formally verify” the correctness of the logic in any sensible way.
As for compilers & solidity - I think that the development of solidity was a mistake. It would be much better to take an already-existing programming language with existing and time-tested toolchain instead of developing a whole new one just for smart-contracts.
Here is my article about the new languages for contracts New programming language for smartcontract is a mistake | EOS Go Blog