This is your work, valued
coq-vyper. A Vyper compiler in Coq (just started)
coq-evm. Hash functions used in EVM implemented in Coq.
coq-yul. Formalization of Yul