Formal Reasoning for Compilers

Aims

Powerful, production-ready compilation frameworks, such as LLVM and MLIR, are embodied in 10 million lines of C++. They are open not only in the sense of accepting contributions from a diverse community, but also they admit numerous extension points for building experimental or non-standard compilation toolchains.

LLVM and MLIR's size and extensibility make them extremely challenging, semantically. In recent years their communities have faced real difficulties in areas such as undefined behaviour, floating point corner cases, and pointer provenance, as well as the never-ending growth of hand-written optimiser logic with limited ability to verify the invariants it aims to maintain.

It seems clear that we can do better than embodying compiler semantics in an English-language LangRef and in millions of lines of hand-written code. We explore the following ideas:

• Compiler development should be semantics-first. Machine-readable semantics should guide day-to-day development, support high-productivity tooling and automation, and provide a previously unseen level of trust.
• To whatever extent possible, compiler internals should be synthesised using both formal methods for correctness and data-driven methods to identify which analyses and optimisations are worthwhile in practice.
• The built-in extensibility of MLIR already serves as a basis for radical innovation in compiler IRs. Combined with formal semantics, program synthesis, and data-driven optimisation tuning, creating a new verified IR should take days or weeks rather than months.
• We need a path from academic exploration to industrial use of formal methods. Instead of building abstract models of key ideas, we need to move towards building day-to-day helpers, detailed formal twins, and formal-first products.

Alive2 demonstrated success as a day-to-day helper. Formal twins must be scalable, both in complexity and runtime, and formal-first products must align with established community and industrial needs.

Syllabus

You will directly contribute to a fork of VeIR, a young open-source project working towards building a formal twin of LLVM and MLIR.

The repository is maintained by a small but active community led by the course organisers, with experience of integrating student work into its code base. All code is developed following industry best practice, including code review and human-crafted commit messages.

You are expected to participate actively in code review, both receiving and giving reviews. You will learn how to develop your code open-source-first, in small increments that eventually lead to important new features for VeIR.

The Git repository is maintained by our research group as an open-source project, allowing us to offer realistic review experience in a safe environment. We will work with you to coordinate your contributions with the community, plan the size, timelines and process of your contributions, and arrange peer review.

We also allow the use of LLMs in development, embrace agentic loops and large-scale synthesis, and may offer compute from namespace.so and Anthropic. We use peer code review and Lean-certified correctness to ensure high code quality.

Our ultimate objective is the formal verification of LLVM and MLIR. This means that we run our research programme in a startup-style manner, with clear technical directions and a consistent focus on impact rather than blue-sky research.

Potential lectures

• Modern SSA-Based Register Allocation
• Translation Validation in LLVM and MLIR using Alive
• ISA Specification in Industry
• Bit-level Reasoning in Compilers
• Declarative Rewriting

Assessment

Essay 1: 200 words, 10%

• Proposed research objective for an individual mini-project.
• Written formative feedback on the proposal from course organisers.

Essay 2: 400 words, 20%

• Confirmed research objective and work plan, including relevant citations to prior publications.

Essay 3: 1,000 words, 60%

• Evaluation of the student's own contribution, together with peer review comparing their contribution with the contributions of one or two other students.

Class presentation: 10%

Recommended reading

• SSA Based Compiler Design
• LLVM Code Generation: A Deep Dive Into Compiler Backend Development
• Theorem Proving in Lean 4

MLIR website

VeIR website