alive2 ☆

« Back to VersTracker

Description:
Automatic verification of LLVM optimizations

Type: Formula | Latest Version: 21.0@1 | Tracked Since: Dec 17, 2025

Links: Homepage | formulae.brew.sh

Category: Developer tools

Tags: llvm verification compiler formal-methods z3 debugging

Install: brew install alive2

About:
Alive2 is a sophisticated tool designed for the automatic formal verification of LLVM compiler optimizations. It systematically tests optimization passes by generating valid programs and transformations, mathematically proving whether an optimization is correct or finding specific counterexamples that expose bugs. This provides a critical safety net for compiler developers, ensuring that performance enhancements do not introduce subtle, critical errors into the generated code.

Key Features:

Automatic formal verification of LLVM IR optimizations
Finds counterexamples to prove incorrect transformations
Generates valid programs to test optimization passes
Integrates with Z3 SMT solver for logical proofs
Supports both Alive and Alive2 languages for specifying transformations

Use Cases:

Verifying correctness of custom LLVM optimization passes
Testing existing compiler optimizations for subtle bugs
Educational tool for learning about compiler transformations and formal verification
Ensuring safety of optimizations in mission-critical or security-sensitive codebases

Alternatives:

LLVM's built-in test suites – Alive2 provides formal mathematical proofs, whereas standard test suites rely on manual test cases and may miss edge cases.
KLEE – KLEE is a symbolic execution engine for finding bugs in programs, while Alive2 is specifically designed to verify the correctness of compiler transformations.

License: MIT

Dependencies: hiredis, llvm, z3, zstd

Bottles available for: arm64_tahoe, arm64_sequoia, arm64_sonoma, arm64_ventura, sonoma, ventura, arm64_linux, x86_64_linux

Version History

Detected	Version	Rev	Change	Commit
Sep 13, 2025 10:10am		1	VERSION_BUMP	2fd7a796