Veriopt
Veriopt is a formal verification effort undertaken by researchers at the University of Queensland. The project aims to formally verify the optimization phases within the GraalVM compiler.
The intermediate representation of the compiler is formalized within the Isabelle/HOL interactive theorem prover. Optimizations are then proven to be semantic preserving transformations of the intermediate representation.
GraalVM offers a unique opportunity to verify a state-of-the-art optimizing compiler.
The GraalVM compiler implements a comprehensive suite of compiler optimizations on a modern intermediate representation.
In addition, as a polyglot compiler which implements futamura projections, we are afforded the unique opportunity of verifying an optimization once and having that optimization applicable to a wide variety of languages.
Our current approach is to encode the GraalVM intermediate representation, semantics, and optimizations into the Isabelle/HOL interactive theorem prover.
We are then able to prove that the transformations of the representation preserve the semantics interactively.