The main focus has been on the formal verifiability of smart contracts written in Michelson -- https://www.michelson-lang.com/ I'm checking on Tezos itself.