Despite being based on semi-functional programming language Scala, I found no evidence that the language AxLang has anything to do with formal verification. I may be wrong, but what I see now is lots of promises without any details.
How do you mean? There are examples of formal verification working in the video. The resulting compiled smart contracts are on the live Ethereum blockchain.