have you attempted to apply any formal methods (coq, isabelle, tla, whatever) to your code? or will you be content with mere auditing?
if i were aware of any material on formalizing solidity or the EVM, honestly i'd keep it to myself and use it to identity vulnerabilities in your contracts. in that hypothetical world, my question was a means to check and see if you were a good target.
good luck. :)