vir

May 5, 2026 · View on GitHub

Human-written summary

vir (verified IR) is a proof-of-concept of a formally-verified compiler. The IR similar to LLVM IR, with the pie-in-the-sky idea that maybe we could eventually have a bidirectional translation LLVM IR <-> vir.

The motivation is, maybe you trust a vibe-coded compiler if it comes with a proof of correctness. And moreover, maybe we can even let the AI make bespoke modifications to a program's IR if it can provide a proof of equivalence along with the modifications.

A production-level formally-verified compiler has previously been infeasible because writing proofs for everything is super annoying. But maybe it's feasible today (or soon) thanks to our superhuman coding assistants. That's the hypothesis, anyway.

This project is currently extremely incomplete and almost completely vibe-coded. I don't know Lean. Please don't judge me.

Everything below is written by AI. Good luck.

The current milestone is a validation-focused IR skeleton:

  • type-safe ValId and BlockId wrappers for table indexes
  • array-backed function tables for values and blocks
  • constants and instructions as Val definitions
  • blocks that store instruction IDs in order
  • instruction payload types with local validation predicates
  • an aggregate Instr type that forwards validation to the payload instance
  • a function-level ValidationCtx that lets instruction invariants avoid importing concrete Function
  • reusable block and instruction dominator analyses for whole-function validation

Layout

  • Vir.IR.*: IR types, IDs, constants, values, blocks, instructions, functions, and aggregate validation predicates
  • Vir.Analysis.DomTree: block-level dominator analysis
  • Vir.Analysis.InstrDomTree: instruction-level dominance analysis
  • Vir.Data.*: reusable data structures and data-oriented proof helpers
  • Vir.FixedPoint.*: reusable terminating fixed-point recursion helpers

Development notes

  • Avoid O(n²) algorithms where a small reusable index or analysis can provide the same information with clearer asymptotic behavior.

Tests

Build and test with:

lake test
lake build