VM formal specification
This is the specification of the instruction set of EraVM 1.4.0, a language virtual machine for ZKsync Era. It describes the virtual machine's architecture, instruction syntax and semantics, and some elements of system protocol.
Please note that the formal specification describes an outdated version of EraVM (pre-boojum), so the usefulness is limited today. While it may be useful for understanding general concepts, and many parts of the implementation remain the same, the specification does not describe the virtual machine used today.