// readme

Vellvm - verified LLVM IR

Vellvm is an ongoing project aiming at the formal verification in the Rocq proof assistant of a compilation infrastructure inspired by the LLVM compiler.

Check out the Vellvm home page for more information.

Installing / Compiling Vellvm

Assumes:

  • OCaml 4.14.1 (typically installed via opam, see below)
  • Rocq 9.1.1
  • opam 2.0.0+
  • Clang 14.0.1+ (available for Mac OSX in XCode 4.2+, or installed via, e.g. sudo apt-get install clang)
  • gnu-sed
    • sed defaults to gnu-sed on linux.
    • for Mac OS X with homebrew, do brew install gnu-sed and then create a symlink from sed to the gsed executable in your path.)

Compilation:

  1. Clone the vellvm git repo
  2. Install all external dependencies
    • Note: you should be able to install all of the opam libraries by running make opam in the src/ directory.
  3. Run make vellvm in the src/ directory: it will produce the OCaml executable called vellvm
    • Note: running just make will also build all of Vellvm’s metatheory, which is necessary for proving things, but takes much longer

opam, Rocq, and opam…

↑ The Undervalued Score +

How much a project earns versus how much attention it actually gets. Above 50 means the work is outrunning its audience. Recomputed nightly from commit velocity, contributor effort, issue resolution, fork utility, release cadence, and project maturity — divided by a logarithmic reach factor.

score  = signal / reach

signal = 0.25·commit_velocity   // commits in last 90 days (cap 30)
       + 0.20·contributor_work  // unique authors × velocity (cap 100)
       + 0.20·issue_resolution  // closed ÷ total issues
       + 0.20·fork_ratio        // forks ÷ stars (proxy for real usage)
       + 0.10·release_cadence   // releases in 90 days (cap 3)
       + age_bonus              // +0 to +0.30 after 6 months
       + homepage_bonus         // +0.05 if homepage is set

reach  = log₁₀(stars + watchers + 10)█
♥ The Health Score +

Is the project alive and maintained right now? A 0–100 pulse recomputed nightly from commit recency, rhythm, how fast issues close, and how quickly PRs get merged.

health = 0.35·recency       // days since last commit (90d decay)
       + 0.25·cadence       // commit rhythm consistency
       + 0.20·issue_health  // closed ÷ total issues
       + 0.20·pr_health     // merged ÷ total PRs█
◷ Health bands +

The colour and label on every card come straight from the health score.

Healthy   80 – 100   active, responsive, regular releases
Stable    60 – 79    maintained, steady, no alarms
Quiet     40 – 59    slowing down — watch this one
At Risk    0 – 39    going dark · candidate for rescue█
// Tags — what each label means +

Tags are independent behavioral signals computed nightly. A project can hold multiple at once. They drive the home page sections.

solo_builder      one person holds > 80% of commits (last 180d)
needs_contributors has open "help wanted" or "good first issue" labels
hidden_gem        < 100 stars · active in last 3 months · documented
legacy_hero       repo > 5 years old · committed this year
fork_magnet       forks/stars > 0.5 · used as template or dependency
release_machine   5+ releases in the last 90 days
under_pressure    > 10 open issues · ≤ 2 contributors · health ≥ 60
community_watch   watchers > stars · devs tracking before the public
community_hub     GitHub Discussions enabled · > 20 discussions
funded            maintainer has active funding channel█
★ Why rank against stars at all? +

Stars are an outcome, not effort. A project with 8 stars and daily commits is doing more interesting work than one coasting on 8k. We measure the building, then divide by the attention already received — so the genuinely undervalued rise to the top.

// stars   = lagging indicator
// commits = leading indicator
// we rank by the leading one█