alive2

{
  "aliases": [],
  "alternatives": [],
  "build_dependencies": [
    "cmake",
    "re2c"
  ],
  "categories": [],
  "caveats": null,
  "conflicts_with": [],
  "dependencies": [
    "hiredis",
    "llvm",
    "z3",
    "zstd"
  ],
  "deprecated": 0,
  "deprecation_reason": null,
  "desc": "Automatic verification of LLVM optimizations",
  "disable_reason": null,
  "disabled": 0,
  "enrichment_fetched_at": "2026-06-20T23:35:22+00:00",
  "first_seen": "2026-06-20T23:34:18+00:00",
  "full_name": "alive2",
  "github_default_branch": "master",
  "github_last_commit_at": "2026-04-27T07:27:23Z",
  "github_readme_excerpt": "Alive2\n======\n\n![Alive2 logo](imgs/alive2.png)\n\nAlive2 consists of several libraries and tools for analysis and verification\nof LLVM code and transformations.\nAlive2 includes the following libraries:\n* Alive2 IR\n* Symbolic executor\n* LLVM \u2192 Alive2 IR converter\n* Refinement check (aka optimization verifier)\n* SMT abstraction layer\n\nIncluded tools:\n* Alive drop-in replacement\n* Translation validation plugins for clang and LLVM\u0027s `opt`\n* Standalone translation validation tool: `alive-tv` ([online](https://alive2.llvm.org))\n* Clang drop-in replacement with translation validation (`alivecc` and\n  `alive++`)\n* An LLVM IR interpreter that is UB precise (`alive-exec`)\n\nFor a technical introduction to Alive2, please see [our paper from\nPLDI 2021](https://web.ist.utl.pt/nuno.lopes/pubs/alive2-pldi21.pdf).\n\n\nWARNING\n-------\nAlive2 does not support inter-procedural transformations. Alive2 may produce\nspurious counterexamples if run with such passes.\n\n\nSponsors\n--------\nWe thank the continuous support of all of our sponsors! Alive2 wouldn\u0027t be possible without their support.\n\n[![Google](imgs/google.svg)](https://research.google)\n\u0026nbsp;\u0026nbsp;\u0026nbsp;\u0026nbsp;\n[![NLNet](imgs/nlnet.svg)](https://nlnet.nl)\n\u0026nbsp;\u0026nbsp;\u0026nbsp;\u0026nbsp;\n[![Woven by Toyota](imgs/woven.svg)](https://woven.toyota)\n\u0026nbsp;\u0026nbsp;\u0026nbsp;\u0026nbsp;\n[![Matter Labs](imgs/matterlabs.svg)](https://matter-labs.io)\n\nIf your company has benefitted from Alive2 (including having a less buggy LLVM), please consider sponsoring our research lab.\n\n\nPrerequisites\n-------------\nTo build Alive2 you need recent versions of:\n* [cmake](https://cmake.org)\n* [gcc](https://gcc.gnu.org)/[clang](https://clang.llvm.org)\n* [re2c](https://re2c.org/)\n* [Z3](https://github.com/Z3Prover/z3)\n* [LLVM](https://github.com/llvm/llvm-project) (optional)\n* [hiredis](https://github.com/redis/hiredis) (optional, needed for caching)\n\n\nBuilding\n--------\n\n```\ngit clone git@github.com:AliveToolkit/alive2.git\ncd alive2\nmkdir build\ncd build\ncmake -GNinja -DCMAKE_BUIL",
  "github_repo": "AliveToolkit/alive2",
  "github_stars": 1121,
  "github_topics": [
    "automatic-verification",
    "llvm",
    "llvm-ir",
    "model-checking",
    "smt",
    "symbolic-execution",
    "translation-validation",
    "verification"
  ],
  "homepage": "https://github.com/AliveToolkit/alive2",
  "homepage_og_description": null,
  "homepage_og_image": null,
  "homepage_title": null,
  "installs_30d": 65,
  "installs_365d": 335,
  "installs_90d": 100,
  "keg_only": 0,
  "keg_only_reason": null,
  "last_seen": "2026-06-20T23:34:18+00:00",
  "license": "MIT",
  "llm_generated_at": null,
  "llm_model": null,
  "name": "alive2",
  "oldnames": [],
  "one_liner": null,
  "optional_dependencies": [],
  "rank_30d": 4139,
  "rank_365d": 6053,
  "rank_90d": 5577,
  "raw_hash": "00d994cb671da4ee",
  "recommended_dependencies": [],
  "revision": 4,
  "ruby_source_path": "Formula/a/alive2.rb",
  "tap": "homebrew/core",
  "test_dependencies": [],
  "uses_from_macos": [],
  "version_head": "HEAD",
  "version_stable": "21.0",
  "versioned_formulae": [],
  "why_use_this": null
}