I like your point about language complexity. Can you point to a language that would fit the simple and verified criteria? I don't really follow the subject, so it would be interesting reading.
You could take inspiration from a system like Dafny or F-* and write your contracts with the assistance of a type system and compiler that generated proofs that your contracts satisfied some postcondition given a precondition. People have already written moderately complicated applications like operating systems in these languages, so there's some evidence they could be applied to contracts on the blockchain.
