I wonder if something like OCaml would be a good choice. It's a safe language with good performance plus it gives you an easier route to formally verify the important parts of it. Cross platform is going to be trickier though.
Hmm, interesting. I wasn't sure if they were only name dropping that formal verification was possible but they say their developers have backgrounds in it. People mention about making Ethereum more secure using formal verification for example but it's not something you can just do as an afterthought.
