Imperative languages can also be formally verified. See the K framework for formal modeling and verification of EVM smart contracts.
Detailed list: https://github.com/leonardoalt/ethereum_formal_verification_...
> Gas price is extremely low.
Beware, the gas price might be low because there is no volume. Binance Smart Chain had a lot of difficulty the past 2 days because they underpriced gas cost and basically DOS-ed themselves:
- https://mobile.twitter.com/PancakeSwap/status/13845099723948...
- https://mobile.twitter.com/peter_szilagyi/status/13848238801...
You missed a very nice example of Tezos adoption, which was the French military police using it to pay sources
https://journalducoin.com/blockchain/actualites-blockchain/u...