This is a formal semantics of Ethereum Virtual Machine (EVM) specialized for gas consumption analysis. This formal model is used for proving termination of any contract on EVM. The model is defined and property are proved using the Isabelle/HOL proof assistant, more precisely Isabelle/HOL 2018. The only assumptions made on EVM are:
Other technical assumptions and abstractions are explained in the theory files. There are two theory files. The two theories differs on a very particular point: how gas is consumed when a contract is called from another one.
abstEvm.thywhere the EVM semantics is based on the reference yellow papers:yellow paper 2014 and yellow paper 2019.
abstEvm2.thywhere the EVM semantics is closer to the implementations of EVM.
The subtle differences between the two are explained in the comments at the beginning of the files.