Vellvm
  • Home
  • About
  • Github
  • Running Tests
  • Structure
  • Research
  • FAQ
Vellvm is a specification of LLVM IR implemented in Rocq. The Vellvm framework provides an abstract semantics aimed at formal verification of LLVM-based software and optimizations passes, along with an executable interpreter suitable for running LLVM IR code for testing purposes. The interpreter is proved to be a valid refinement of the spec.

Recent News

  • Jul 7, 2026 - Vellvm 3.0 Released!

Getting Started

  1. Follow the installation instructions in the README to get the vellvm executable and add it to your $PATH.

  2. Try out vellvm from the command line, e.g., in the root of the project repo:

~/vellvm> vellvm -interpret tests/ll/factorial.ll 
(* -------- Vellvm Test Harness -------- *)
Processing: tests/ll/factorial.ll
Program terminated with: i64 120
  1. Use vellvm -help to list command-line options

Digging Deeper

  • Find the Vellvm source on github

  • Find out more about the Vellvm framework

  • Learn how to run and add test cases

  • Understand the structure of the semantics

  • Take a look at our research papers

  • Check out the FAQ

Related Projects

  • Interaction Trees - interactive, nonterminating, effectful programs in Rocq

  • CTrees - ITrees with nondeterministic choices

  • Helix - A Rocq DSL for high-performance numerical algorithms that compiles to Vellvm

  • DeepSpec - Formal verification research

Acknowledgments

Vellvm is being developed at the University of Pennsylvania with collaborators at Inria.

Recent Contributors

  • Steve Zdancewic
  • Yannick Zakowski
  • Calvin Beck
  • Irene Yoon
  • Gary (Hanxi) Chen
  • Roger Burtonpatel

Funding

Funding for the Vellvm project has been provided by the NSF and DARPA.

See the Research Page for more details.
Last Modified: Jul 7, 2026 12:04 pm