Hi Viet,
I did not work on the formalization of EVM a while ago due to other work
The following is the implementation (not completed) on Github.
However, we are working on the other aspect of EVM code analysis. We want to statically infer an upper-bound on the amount of gas
consumption for all inputs (input arguments and storage configurations). This analysis is based on our previous research on resource bound
analysis for both imperative and functional programs.
We translate EVM byte-code into a kind of control flow graph (CFG). However, due to the unstructured and low level of EVM, I suppose it is
more convenient to infer upper-bound on gas consumption at Solidity source code provided that we have a good gas consumption model for
Solidity language constructs.
Best,
-Van Chan