We have described an Isabelle model and execution semantics for the sophisticated sea-of-nodes graph structure [1]} that is used as the internal representation in the GraalVM optimizing compiler [2]}. Additionally, we have proved several suites of local optimizations correct according to the semantics.
