Hacker GitHub

← All repos

AliveToolkit/alive2

View on GitHub ↗ ★ 1,204 C++

Automatic verification of LLVM optimizations

8 mentions on Hacker News by 8 people: 1 story, 7 comments · first 2021-05-03 · latest 2025-09-03

Mentions per year 8 mentions · busiest year 2023 (3)
20082026
AllStoriesComments NewestTopOldest
  1. …from a deterministic, verified compiler and the approximating behavior of a probabilistic LLM. [1]: https://github.com/AliveToolkit/alive2
    comment by ashton314 · 2025-09-03 · in MIT Study Finds AI Use Reprograms the Brain, Leading to Cognitive Decline
  2. But we do! For llvm there's https://github.com/AliveToolkit/alive2 There are papers like https://people.cs.rutgers.edu/~sn349/papers/cgo19-casmverify... There's https://github.com/google/souper There's…
    comment by viraptor · 2025-07-20 · in FFmpeg devs boast of another 100x leap thanks to handwritten assembly code
  3. …to learn with well-specified IL. The other aimed to formalize LLVM’s IL. http://c9x.me/compile/ https://github.com/AliveToolkit/alive2 There have also been typed, assembly languages to support verification from groups like FLINT. One can…
    comment by nickpsecurity · 2024-05-04 · in CBMC: C bounded model checker (2021)
  4. …think it might even be possible to make this work for 64-bit vectors with SMT (in most cases). [1] https://github.com/AliveToolkit/alive2
    comment by someplaceguy · 2023-11-15 · in Haroldbot, client-side tool that checks 32-bit bitvector arithmetic equivalence
  5. …addition to computational constraints. With a lot of time and effort it can be done though [2]. 1. https://github.com/AliveToolkit/alive2 2. https://sel4.systems/
    comment by boomanaiden154 · 2023-05-15 · in Basic SAT model of x86 instructions using Z3, autogenerated from Intel docs
  6. …used for years (almost a decade actually) by people to verify LLVM instcombine transforms. Alive2 ( https://github.com/AliveToolkit/alive2 ) makes it easier to do the same with most optimization passes.
    comment by DannyBee · 2022-11-04 · in Verifying GCC optimizations using an SMT solver
  7. …one of the most famous frameworks for compiler transformation verification using BitVec logic [1] https://github.com/AliveToolkit/alive2
    comment by mshockwave · 2021-05-03 · in Programming in Z3 by learning to think like a compiler