KEVM Virtual Machine
From the website:
"KEVM is a high-quality, formally-verified smart contract virtual machine compatible with the Ethereum virtual machine (EVM). Formally specified in the K framework, the KEVM uses formal semantics for elements such as the configuration and transition rules of EVM, resulting in a more secure virtual machine for smart contracts. IOHK paused its collaboration in the K framework project in order to focus on other priorities, but is enthusiastic about the vision and may participate again in the future.