"formally verify the contract" it would help if Solidity was as well though out as Ada, and not something more like JS.

I'd even argue that imperative programming is the wrong paradigm for such smart contracts.