Публічний реєстрПомірний
Звіт про здоров'я програмного забезпеченнясхема 0.27.0 · метрики 1.13.0 · 2026-07-23 15:29 UTC
prove-rs / z3.rs
Rust bindings for the Z3 solver.
prove-rs/z3.rs має індекс здоров’я 69 зі 100, що відповідає смузі «Помірний». Найвищий показник — Vitality (89/100), найнижчий — AI Readiness (53/100). Останнє оновлення — сьогодні. Більшість нещодавньої роботи виконують 3 учасники.
69
загалом / 100Індекс здоров'я програмного забезпечення
Метрики згруповано у зважені категорії на шкалі 1–100. Загальна оцінка починається як їхнє середнє; коли публічні дані активують Політику юрисдикцій високого ризику, рейтинг коригується й отримує верхню межу 49 («Під ризиком»). Готовність до ШІ не входить до індексу.
69
Відмінний85-100Зразковий; відповідає практично всім перевіреним критеріям
Добрий70-84Здоровий; незначні прогалини
Помірний50-69Прийнятний, але з помітними прогалинами; рекомендовано перевірку
У зоні ризику30-49Суттєві слабкі місця; впровадження потребує обережності
Критичний1-29Серйозні проблеми (покинутий, єдиний мейнтейнер, без базової гігієни)
Профіль оцінок
Кожна вісь — окрема категорія. Форма важить більше, ніж середнє: здоровий об'єкт заповнює всю фігуру, тоді як профіль із піками та провалами означає, що сила в одному вимірі маскує ризик в іншому.
Власність
prove-rsОрганізація
5 підписників2 публічні репозиторіїз квіт. 2018 р.
За цим репозиторієм стоїть організація — спільна, підзвітна опіка, здатна пережити будь-якого окремого мейнтейнера.
Пакетні екосистеми
| Реєстр | Пакет | Версія | Завантажень / міс | Версії | Остання публікація | Теги |
|---|---|---|---|---|---|---|
| crates.io | z3 | 0.20.2 | 164 435 | 55 | 26 днів тому | ffisolversmtsatisfiabilityapi-bindings |
| crates.io | xtaskвказує на інший репозиторій — не оцінюється | 0.1.4 | 185 | 5 | 23 дні тому | automationmacosreleasecodesignxtaskcommand-line-utilities |
| crates.io | z3-src | 500.0.0 | 9 492 | 10 | 0 днів тому | solverbuildsmtsatisfiability |
| crates.io | z3-sys | 0.12.0 | 165 755 | 36 | 0 днів тому | ffisolversmtsatisfiabilityno-stdexternal-ffi-bindings |
Метрики за категоріями
Життєздатність
Чи живий проєкт — чи пишеться код і чи виходять релізи?
89
Активність розробки
81Добрий
Як обчислюється оцінка
| 36/36 | Свіжість push — останній push 0 дн. тому |
| 17.3/36 | Ритм комітів — 25/52 тижнів із комітами |
| 18/18 | Обсяг комітів — 114 комітів за останній рік |
| 10/10 | OpenSSF Scorecard: Maintained — 10 commit(s) and 4 issue activity found in the last 90 days -- score normalized to 10 |
Використані вхідні дані
| commits_last_year | 114 |
| human_commit_share | 1 |
| days_since_last_push | 0 |
| active_weeks_last_year | 25 |
Дисципліна релізів
100Відмінний
Як обчислюється оцінка
| 27/27 | Випускає релізи — опубліковано 61 релізів |
| 36/36 | Свіжість релізів — останній реліз 0 дн. тому |
| 27/27 | Ритм релізів — реліз кожні ~14,7 дн. |
| 0/10 | OpenSSF Scorecard: Signed-Releases — немає даних |
Використані вхідні дані
| releases_count | 61 |
| latest_release_tag | z3-sys-v0.12.0 |
| releases_from_tags | ні |
| days_since_latest_release | 0 |
| mean_days_between_releases | 14,7 |
Виключено з оцінювання (немає даних або не застосовно): OpenSSF Scorecard: Signed-Releases. Залишкові ваги перенормовано.
Спільнота та впровадження
Чи має проєкт користувачів, завантаження, увагу та влаштовані умови для контриб’юторів?
58
Популярність і впровадження
66Помірний
Як обчислюється оцінка
| 44.1/60 | Зірки — 522 зірок |
| 18.2/25 | Форки — 153 форків |
| 3.9/15 | Спостерігачі — 6 спостерігачів |
Використані вхідні дані
| forks | 153 |
| stars | 522 |
| watchers | 6 |
| growth_state | unverified |
| growth_factor_pct | 100 |
| growth_unverified_reason | no_history |
Здоров'я спільноти
25Критичний
Як обчислюється оцінка
| 22.5/22.5 | README |
| 0/22.5 | Ліцензія — файлу ліцензії не виявлено |
| 0/18 | Настанови CONTRIBUTING |
| 0/13.5 | Кодекс поведінки |
| 0/7.2 | Шаблон issue |
| 0/6.3 | Шаблон PR |
Використані вхідні дані
| has_readme | так |
| has_license | ні |
| has_contributing | ні |
| has_issue_template | ні |
| has_code_of_conduct | ні |
| has_pull_request_template | ні |
Впровадження в екосистемі (завантаження)
92Відмінний
Як обчислюється оцінка
| 73.7/80 | Щомісячні завантаження — 339 682 завантажень/місяць у crates |
| 0/20 | Залежні пакети в реєстрі — ця екосистема цього не повідомляє |
Використані вхідні дані
| packages | z3, z3-src, z3-sys |
| dependents | — |
| ecosystems | crates |
| total_downloads | 3 061 744 |
| monthly_downloads | 339 682 |
Виключено з оцінювання (немає даних або не застосовно): Залежні пакети в реєстрі. Залишкові ваги перенормовано.
Сталість та врядування
Чи переживе проєкт своїх людей — бас-фактор, реактивність, хто за ним стоїть і як супроводжуються пакети?
74
Як обчислюється оцінка
| 36/54 | Бас-фактор — на 3 контриб’ютор(ів) припадає половина всіх комітів |
| 15.5/22.5 | Розподіл комітів — головний контриб’ютор — автор 31% комітів |
| 13.5/13.5 | Широта контриб’юторів — 78 контриб’юторів |
| 10/10 | OpenSSF Scorecard: Contributors — project has 26 contributing companies or organizations |
Використані вхідні дані
| bus_factor | 3 |
| contributors_sampled | 78 |
| top_contributor_share | 0,309 |
Реактивність на issue та PR
74Добрий
Як обчислюється оцінка
| 37.3/46.8 | Вирішення issue — закрито 80% issue |
| 34.2/38.3 | Прийняття PR — злито 328/367 вирішених PR |
| 3/15 | OpenSSF Scorecard: Code-Review — Found 6/30 approved changesets -- score normalized to 2 |
Використані вхідні дані
| merged_prs | 328 |
| open_issues | 37 |
| closed_issues | 145 |
| issue_closed_ratio | 0,797 |
| closed_unmerged_prs | 39 |
Власність та опіка
51Помірний
Як обчислюється оцінка
| 30/30 | Підтримка власника — у власності організації |
| 0/20 | Верифікований домен |
| 5.6/25 | Охоплення власника — 5 підписників у prove-rs |
| 15.5/25 | Послужний список — 2 публічних репозиторіїв, вік облікового запису ~8 р. |
Використані вхідні дані
| followers | 5 |
| owner_type | Organization |
| is_verified | — |
| owner_login | prove-rs |
| public_repos | 2 |
| account_age_days | 3 017 |
Супровід пакетів
100Відмінний
Як обчислюється оцінка
| 25/25 | Опубліковано й доступно — 3 пакет(ів) у crates |
| 35/35 | Свіжість публікацій — остання публікація 0 дн. тому |
| 20/20 | Історія версій — 55 опублікованих версій |
| 20/20 | Не застарілий — активний, не deprecated і не yanked |
Використані вхідні дані
| packages | z3, z3-src, z3-sys |
| ecosystems | crates |
| any_deprecated | ні |
| min_days_since_publish | 0 |
Інженерна якість
Чи наявні базові інженерні практики та документація?
64
Інженерні практики
66Помірний
Як обчислюється оцінка
| 24/24 | Процеси CI — 3 процес(ів) CI |
| 24/24 | Наявні тести |
| 0/16 | Конфігурація лінтера |
| 0/9.6 | Pre-commit-хуки |
| 0/6.4 | .editorconfig |
| 18/20 | OpenSSF Scorecard: CI-Tests — 25 out of 27 merged PRs checked by a CI test -- score normalized to 9 |
Використані вхідні дані
| has_ci | так |
| has_tests | так |
| has_editorconfig | ні |
| has_linter_config | ні |
| has_precommit_config | ні |
Документація
60Помірний
Як обчислюється оцінка
| 30/30 | README |
| 0/25 | Каталог документації |
| 0/15 | Сайт документації / домашня сторінка |
| 10/10 | Опис репозиторію |
| 10/10 | Теми — 6 тем |
| 10/10 | Wiki |
Використані вхідні дані
| topics | logic-programming, smt, smt-solver, rust-bindings, rust, ffi-bindings |
| has_wiki | так |
| homepage | — |
| has_readme | так |
| has_docs_dir | ні |
| has_description | так |
Безпека
Чи міцні видимі практики безпеки й ланцюга постачання, без непослабленої пов’язаності з юрисдикціями високого ризику?
54
Стан безпеки
42У зоні ризику
Як обчислюється оцінка
| 7.5/7.5 | Binary-Artifacts — no binaries found in the repo |
| 0/7.5 | Branch-Protection — branch protection not enabled on development/release branches |
| 2.2/2.5 | CI-Tests — 25 out of 27 merged PRs checked by a CI test -- score normalized to 9 |
| 0/2.5 | CII-Best-Practices — no effort to earn an OpenSSF best practices badge detected |
| 1.5/7.5 | Code-Review — Found 6/30 approved changesets -- score normalized to 2 |
| 2.5/2.5 | Contributors — project has 26 contributing companies or organizations |
| 10/10 | Dangerous-Workflow — no dangerous workflow patterns detected |
| 0/7.5 | Dependency-Update-Tool — no update tool detected |
| 0/5 | Fuzzing — project is not fuzzed |
| 0/2.5 | Ліцензія — license file not detected |
| 7.5/7.5 | Maintained — 10 commit(s) and 4 issue activity found in the last 90 days -- score normalized to 10 |
| 0/5 | Packaging — немає даних |
| 0/5 | Pinned-Dependencies — dependency not pinned by hash detected -- score normalized to 0 |
| 0/5 | SAST — SAST tool is not run on all commits -- score normalized to 0 |
| 0/5 | Security-Policy — security policy file not detected |
| 0/7.5 | Signed-Releases — немає даних |
| 0/7.5 | Token-Permissions — detected GitHub workflow tokens with excessive permissions |
| 7.5/7.5 | Vulnerabilities — 0 existing vulnerabilities detected |
Використані вхідні дані
| source | openssf_scorecard |
| checks_evaluated | 16 |
| scorecard_version | v5.5.0 |
| checks_inconclusive | 2 |
| scorecard_aggregate | 4,2 |
Виключено з оцінювання (немає даних або не застосовно): packaging, signed_releases. Залишкові ваги перенормовано.
Сповіщення про залежності
100Відмінний
Як обчислюється оцінка
| 35/35 | Прямі залежності без відомих сповіщень — жодна пряма залежність не має відомих сповіщень |
| 25/25 | Непрямі залежності без відомих сповіщень — жодна непряма залежність не має відомих сповіщень |
| 0/40 | Немає задавнених сповіщень — жодне сповіщення не має дати публікації |
Використані вхідні дані
| source | osv |
| advisories | 0 |
| affected_packages | 0 |
| assessed_packages | 20 |
| unassessed_packages | 0 |
| affected_by_severity | none |
| direct_affected_packages | 0 |
Виключено з оцінювання (немає даних або не застосовно): Немає задавнених сповіщень. Залишкові ваги перенормовано. Звірено з runtime-замиканням залежностей crates:z3@0.20.2 — тим, що тягне за собою встановлення опублікованого пакета, — 20 пакетів. Досяжність не аналізується.
Готовність до ШІ
Наскільки репозиторій оснащений для розробки та супроводу за участі ШІ-агентів? Незалежний, експериментальний бейдж — вага 0.0, тож він подається окремо і не впливає на загальний індекс здоров'я.
53
Контекст і настанови для агентів
40У зоні ризику
Як обчислюється оцінка
| 0/45 | Інструкції для агентів — немає CLAUDE.md / AGENTS.md / правил редактора |
| 0/15 | Машиночитана документація (llms.txt) |
| 40/40 | Читабельна історія комітів — намір зазначено у 99 з 100 людських комітів (структурований заголовок або пояснювальний текст) |
Використані вхідні дані
| has_llms_txt | ні |
| legible_history_share | 0,99 |
| agent_instruction_files | — |
| agent_instruction_max_bytes | — |
Цикл верифікації (збірка / тести / перевірка типів)
46У зоні ризику
Як обчислюється оцінка
| 12.6/18 | Розгортання однією командою — Cargo.toml, xtask/Cargo.toml, z3-src/Cargo.toml (домовленість інструментарію, без раннера задач) |
| 22/22 | Автоматизовані тести |
| 0/11 | Конфігурація лінтера / форматера |
| 11/11 | Статична перевірка типів — Rust (статично типізована) |
| 0/10 | Відтворюване середовище |
| 0/10 | Підтверджена практика роботи з агентами — серед останніх 100 комітів немає створених агентом |
| 0/8 | Автоматизоване супроводження — автоматичних оновлень залежностей не виявлено |
| 0/10 | OpenSSF Scorecard: Pinned-Dependencies — dependency not pinned by hash detected -- score normalized to 0 |
Використані вхідні дані
| has_nix | ні |
| has_tests | так |
| lockfiles | — |
| has_dockerfile | ні |
| typed_language | так |
| bootstrap_files | — |
| has_devcontainer | ні |
| has_linter_config | ні |
| typecheck_configs | — |
| agent_commit_share | 0 |
| toolchain_manifests | Cargo.toml, xtask/Cargo.toml, z3-src/Cargo.toml, z3-sys/Cargo.toml, z3/Cargo.toml |
| dependency_bot_commit_share | 0 |
Читабельність коду для моделей
100Відмінний
Як обчислюється оцінка
| 45/45 | Типізований код — Rust (статично типізована) |
| 55/55 | Керовані розміри файлів — 0/64 файлів вихідного коду понад 60 КБ |
Використані вхідні дані
| primary_language | Rust |
| largest_source_bytes | 56 019 |
| source_files_sampled | 64 |
| oversized_source_files | 0 |
Ключові факти
522зірок GitHub
78контриб'юторів
114комітів за останні 12 місяців
0днів від останнього пушу
61релізів
3бас-фактор
37відкритих issue
crates.ioпакетних екосистем
Попередження щодо збору даних
- Star history unavailable: GitHub GraphQL error: Resource not accessible by personal access token
- crates package 'xtask' points at a different repository (https://github.com/arcboxlabs/xtask); excluded from ecosystem scoring
Докладніше
Історія зірок і форків 0 ★ / 153 ⇿
0Зірки
153Форки
58Релізи
Коли додано кожну зірку й форк — зібрано з GitHub і згруповано за днями. Кумулятивне зростання розміщено просто над денними додаваннями, з яких воно складається, тож їх видно одне проти одного: рівномірне органічне накопичення виглядає зовсім інакше, ніж різкий короткочасний сплеск. Там, де цю різницю можна виміряти, її подано як автентичність росту.
Мажорні 0Мінорні 0Патчі 0
Кожна точка охоплює 8 днів.
OpenSSF Scorecard 4.2 / 10
4.2сукупно
Незалежна, не прив'язана до інструментів оцінка безпеки від відкритого проєкту OpenSSF Scorecard. Кожна перевірка винагороджує практику безпеки, а не інструмент конкретного постачальника. Перевірки, які Scorecard не зміг визначити, позначено н/д і виключено з оцінки безпеки (вони ніколи не зараховуються як нуль).
| 10 | Binary-Artifacts | no binaries found in the repo |
| 0 | Branch-Protection | branch protection not enabled on development/release branches |
| 9 | CI-Tests | 25 out of 27 merged PRs checked by a CI test -- score normalized to 9 |
| 0 | CII-Best-Practices | no effort to earn an OpenSSF best practices badge detected |
| 2 | Code-Review | Found 6/30 approved changesets -- score normalized to 2 |
| 10 | Contributors | project has 26 contributing companies or organizations |
| 10 | Dangerous-Workflow | no dangerous workflow patterns detected |
| 0 | Dependency-Update-Tool | no update tool detected |
| 0 | Fuzzing | project is not fuzzed |
| 0 | License | license file not detected |
| 10 | Maintained | 10 commit(s) and 4 issue activity found in the last 90 days -- score normalized to 10 |
| н/д | Packaging | packaging workflow not detected |
| 0 | Pinned-Dependencies | dependency not pinned by hash detected -- score normalized to 0 |
| 0 | SAST | SAST tool is not run on all commits -- score normalized to 0 |
| 0 | Security-Policy | security policy file not detected |
| н/д | Signed-Releases | no releases found |
| 0 | Token-Permissions | detected GitHub workflow tokens with excessive permissions |
| 10 | Vulnerabilities | 0 existing vulnerabilities detected |
Прямі залежності 6
| Реєстр | Пакет | Обмеження версії | Маніфест |
|---|---|---|---|
| crates.io | clap | 4.6 | xtask/Cargo.toml |
| crates.io | semver | 1 | xtask/Cargo.toml |
| crates.io | cmake | 0.1.54 | z3-src/Cargo.toml |
| crates.io | log | 0.4 | z3/Cargo.toml |
| crates.io | num | 0.4 | z3/Cargo.toml |
| crates.io | z3-sys | 0.12.0 | z3/Cargo.toml |
Усі залежності 20
Повний розв'язаний набір залежностей із графа залежностей GitHub: 6 прямих і 14 непрямих (транзитивних) пакетів. Транзитивне замикання є повним, коли в репозиторії закомічено lockfile.
| Реєстр | Пакет | Версія | Зв'язок |
|---|---|---|---|
| crates.io | clap | — | пряма |
| crates.io | cmake | — | пряма |
| crates.io | log | — | пряма |
| crates.io | num | — | пряма |
| crates.io | semver | — | пряма |
| crates.io | z3-sys | — | пряма |
| crates.io | bindgen | — | непряма |
| crates.io | env_logger | — | непряма |
| crates.io | pkg-config | — | непряма |
| crates.io | prettyplease | — | непряма |
| crates.io | proc-macro2 | — | непряма |
| crates.io | quote | — | непряма |
| crates.io | rayon | — | непряма |
| crates.io | regex | — | непряма |
| crates.io | reqwest | — | непряма |
| crates.io | serde_json | — | непряма |
| crates.io | syn | — | непряма |
| crates.io | vcpkg | — | непряма |
| crates.io | z3-src | — | непряма |
| crates.io | zip | — | непряма |
Сповіщення про залежності 0
Встановлення crates:z3@0.20.2 тягне 20 пакетів, прямих і транзитивних: 0 мають відомі сповіщення, з них 0 — прямі залежності.
Жодне відоме сповіщення не стосується оцінених залежностей.
Сповіщення означає, що версія, записана в графі залежностей, потрапляє в уражений діапазон. Досяжність не аналізується, а граф містить піниї розробки й тестування — знахідка може стосуватися інструментів, а не поставленого коду.
Звіт у форматі JSON машиночитний
{
"data": {
"repo": {
"topics": [
"logic-programming",
"smt",
"smt-solver",
"rust-bindings",
"rust",
"ffi-bindings"
],
"is_fork": false,
"size_kb": 1279,
"has_wiki": true,
"homepage": null,
"languages": {
"C": 16,
"Rust": 819429
},
"pushed_at": "2026-07-23T11:47:09Z",
"created_at": "2018-03-08T16:19:05Z",
"owner_type": "Organization",
"updated_at": "2026-07-23T11:46:20Z",
"description": "Rust bindings for the Z3 solver.",
"is_archived": false,
"is_disabled": false,
"license_spdx": null,
"default_branch": "master",
"license_spdx_raw": null,
"primary_language": "Rust",
"significant_languages": [
"Rust"
]
},
"owner": {
"blog": null,
"name": null,
"type": "Organization",
"login": "prove-rs",
"company": null,
"location": null,
"followers": 5,
"avatar_url": "https://avatars.githubusercontent.com/u/38518140?v=4",
"created_at": "2018-04-19T04:47:55Z",
"is_verified": null,
"public_repos": 2,
"account_age_days": 3017
},
"license": {
"state": "absent",
"spdx_id": null,
"raw_spdx": null,
"file_present": false,
"scorecard_found": false,
"profile_has_license": false
},
"activity": {
"releases": [
{
"tag": "z3-sys-v0.12.0",
"kind": "other",
"published_at": "2026-07-23T11:42:00Z"
},
{
"tag": "z3-src-v500.0.0",
"kind": "other",
"published_at": "2026-07-22T19:00:08Z"
},
{
"tag": "z3-v0.20.2",
"kind": "other",
"published_at": "2026-06-26T18:26:26Z"
},
{
"tag": "z3-v0.20.1",
"kind": "other",
"published_at": "2026-06-21T16:59:59Z"
},
{
"tag": "z3-src-v416.0.2",
"kind": "other",
"published_at": "2026-04-12T17:45:54Z"
},
{
"tag": "z3-v0.20.0",
"kind": "other",
"published_at": "2026-04-01T18:31:59Z"
},
{
"tag": "z3-sys-v0.11.0",
"kind": "other",
"published_at": "2026-04-01T18:31:51Z"
},
{
"tag": "z3-v0.19.15",
"kind": "other",
"published_at": "2026-03-20T00:11:49Z"
},
{
"tag": "z3-v0.19.14",
"kind": "other",
"published_at": "2026-03-13T10:30:30Z"
},
{
"tag": "z3-sys-v0.10.9",
"kind": "other",
"published_at": "2026-03-13T10:30:18Z"
},
{
"tag": "z3-v0.19.13",
"kind": "other",
"published_at": "2026-03-06T19:35:54Z"
},
{
"tag": "z3-sys-v0.10.8",
"kind": "other",
"published_at": "2026-03-06T19:35:44Z"
},
{
"tag": "z3-v0.19.12",
"kind": "other",
"published_at": "2026-03-04T13:22:11Z"
},
{
"tag": "z3-v0.19.11",
"kind": "other",
"published_at": "2026-02-27T09:03:59Z"
},
{
"tag": "z3-v0.19.10",
"kind": "other",
"published_at": "2026-02-24T10:10:20Z"
},
{
"tag": "z3-sys-v0.10.7",
"kind": "other",
"published_at": "2026-02-24T10:10:09Z"
},
{
"tag": "z3-v0.19.9",
"kind": "other",
"published_at": "2026-02-21T20:33:39Z"
},
{
"tag": "z3-sys-v0.10.6",
"kind": "other",
"published_at": "2026-02-21T20:33:29Z"
},
{
"tag": "z3-v0.19.8",
"kind": "other",
"published_at": "2026-02-13T12:43:40Z"
},
{
"tag": "z3-sys-v0.10.5",
"kind": "other",
"published_at": "2026-02-13T12:43:28Z"
},
{
"tag": "z3-v0.19.7",
"kind": "other",
"published_at": "2025-12-27T13:36:32Z"
},
{
"tag": "z3-sys-v0.10.4",
"kind": "other",
"published_at": "2025-12-27T13:36:16Z"
},
{
"tag": "z3-v0.19.6",
"kind": "other",
"published_at": "2025-12-10T17:44:41Z"
},
{
"tag": "z3-v0.19.5",
"kind": "other",
"published_at": "2025-11-20T22:02:16Z"
},
{
"tag": "z3-sys-v0.10.3",
"kind": "other",
"published_at": "2025-11-20T22:02:01Z"
},
{
"tag": "z3-v0.19.4",
"kind": "other",
"published_at": "2025-11-18T00:07:55Z"
},
{
"tag": "z3-sys-v0.10.2",
"kind": "other",
"published_at": "2025-11-18T00:07:43Z"
},
{
"tag": "z3-v0.19.3",
"kind": "other",
"published_at": "2025-11-16T21:27:29Z"
},
{
"tag": "z3-sys-v0.10.1",
"kind": "other",
"published_at": "2025-11-16T21:27:16Z"
},
{
"tag": "z3-v0.19.2",
"kind": "other",
"published_at": "2025-10-21T13:35:23Z"
},
{
"tag": "z3-v0.19.1",
"kind": "other",
"published_at": "2025-09-26T18:43:35Z"
},
{
"tag": "z3-v0.19.0",
"kind": "other",
"published_at": "2025-09-26T11:51:16Z"
},
{
"tag": "z3-sys-v0.10.0",
"kind": "other",
"published_at": "2025-09-26T11:50:31Z"
},
{
"tag": "z3-v0.18.2",
"kind": "other",
"published_at": "2025-09-10T14:19:55Z"
},
{
"tag": "z3-v0.18.1",
"kind": "other",
"published_at": "2025-09-09T12:33:23Z"
},
{
"tag": "z3-v0.18.0",
"kind": "other",
"published_at": "2025-09-08T13:10:12Z"
},
{
"tag": "z3-sys-v0.9.10",
"kind": "other",
"published_at": "2025-09-08T13:09:48Z"
},
{
"tag": "z3-v0.17.0",
"kind": "other",
"published_at": "2025-09-03T14:59:18Z"
},
{
"tag": "z3-sys-v0.9.9",
"kind": "other",
"published_at": "2025-09-03T14:58:56Z"
},
{
"tag": "z3-v0.16.2",
"kind": "other",
"published_at": "2025-08-25T22:20:17Z"
},
{
"tag": "z3-sys-v0.9.8",
"kind": "other",
"published_at": "2025-08-25T22:19:57Z"
},
{
"tag": "z3-v0.16.1",
"kind": "other",
"published_at": "2025-08-23T21:38:30Z"
},
{
"tag": "z3-v0.16.0",
"kind": "other",
"published_at": "2025-08-21T10:07:15Z"
},
{
"tag": "z3-v0.15.0",
"kind": "other",
"published_at": "2025-08-19T23:46:44Z"
},
{
"tag": "z3-v0.14.4",
"kind": "other",
"published_at": "2025-08-19T09:09:46Z"
},
{
"tag": "z3-sys-v0.9.7",
"kind": "other",
"published_at": "2025-08-19T09:09:24Z"
},
{
"tag": "z3-v0.14.3",
"kind": "other",
"published_at": "2025-08-18T08:17:57Z"
},
{
"tag": "z3-v0.14.2",
"kind": "other",
"published_at": "2025-08-14T14:04:10Z"
},
{
"tag": "z3-sys-v0.9.6",
"kind": "other",
"published_at": "2025-08-14T14:03:47Z"
},
{
"tag": "z3-v0.14.1",
"kind": "other",
"published_at": "2025-08-10T22:34:42Z"
},
{
"tag": "z3-v0.14.0",
"kind": "other",
"published_at": "2025-08-06T16:54:00Z"
},
{
"tag": "z3-sys-v0.9.5",
"kind": "other",
"published_at": "2025-08-06T16:53:38Z"
},
{
"tag": "z3-v0.13.3",
"kind": "other",
"published_at": "2025-07-17T09:04:01Z"
},
{
"tag": "z3-sys-v0.9.4",
"kind": "other",
"published_at": "2025-07-17T09:03:39Z"
},
{
"tag": "z3-v0.13.2",
"kind": "other",
"published_at": "2025-07-14T18:41:37Z"
},
{
"tag": "z3-sys-v0.9.3",
"kind": "other",
"published_at": "2025-07-14T18:41:14Z"
},
{
"tag": "z3-sys-v0.9.2",
"kind": "other",
"published_at": "2025-07-12T10:17:05Z"
},
{
"tag": "z3-v0.13.1",
"kind": "other",
"published_at": "2025-07-11T08:04:40Z"
},
{
"tag": "z3-sys-v0.9.1",
"kind": "other",
"published_at": "2025-07-11T08:04:11Z"
},
{
"tag": "z3-v0.13.0",
"kind": "other",
"published_at": "2025-07-10T12:36:39Z"
},
{
"tag": "z3-sys-v0.9.0",
"kind": "other",
"published_at": "2025-07-10T12:36:12Z"
}
],
"recent_commits": [
{
"oid": "e717cdd1275333e6b3529b60b8d12d12ab121853",
"body": null,
"is_bot": false,
"headline": "chore: bump z3 to use z3-sys 0.12.0 (#575)",
"author_name": "Mark DenHoed",
"author_login": "toolCHAINZ",
"committed_at": "2026-07-23T11:46:15Z",
"body_truncated": false,
"is_coding_agent": false
},
{
"oid": "60eae85ec4e56561faae56cea155f545aa93ccb0",
"body": "* chore: release\n\n* revert z3 bump to avoid releasing high bindings\n\n* add note to changelog",
"is_bot": false,
"headline": "chore(z3-sys): release v0.12.0 (#571)",
"author_name": "Mark DenHoed",
"author_login": "toolCHAINZ",
"committed_at": "2026-07-23T11:41:17Z",
"body_truncated": false,
"is_coding_agent": false
},
{
"oid": "aade17987951d2dfc810628450cb1216a230b168",
"body": null,
"is_bot": false,
"headline": "chore: allow manual workflow dispatch for builds (#573)",
"author_name": "Mark DenHoed",
"author_login": "toolCHAINZ",
"committed_at": "2026-07-23T10:59:39Z",
"body_truncated": false,
"is_coding_agent": false
},
{
"oid": "0011f9eb16e71e8198592f6f6fd465c6ad3e87bf",
"body": "* updated generated bindings\n\n* fix: bump ci z3 to 5 on linux and mac\n\n* fix: target proper vendored z3-src\n\n* chore: bump gh-release z3 version",
"is_bot": false,
"headline": "chore!: updated z3-sys generated bindings for z3 5 (#572)",
"author_name": "Mark DenHoed",
"author_login": "toolCHAINZ",
"committed_at": "2026-07-22T19:33:58Z",
"body_truncated": false,
"is_coding_agent": false
},
{
"oid": "7e5fbfce2a766d483695c1d5faa0d5eef06d6759",
"body": null,
"is_bot": false,
"headline": "chore: release z3-src (Z3 z3-5.0.0) (#570)",
"author_name": "Mark DenHoed",
"author_login": "toolCHAINZ",
"committed_at": "2026-07-22T18:59:27Z",
"body_truncated": false,
"is_coding_agent": false
},
{
"oid": "55f5737a9a84329ee9bd346c40b144bfdf5245df",
"body": null,
"is_bot": false,
"headline": "chore(z3): release v0.20.2 (#566)",
"author_name": "Mark DenHoed",
"author_login": "toolCHAINZ",
"committed_at": "2026-06-26T18:25:52Z",
"body_truncated": false,
"is_coding_agent": false
},
{
"oid": "7413132783c0d4519c6374ec0f987c69ad5959e1",
"body": "Real::from_rational takes i64 num/den but lowered them via Z3_mk_real, whose C\nsignature is (int, int). Casting the i64 args to c_int silently truncated any\nvalue outside the i32 range: e.g. 634909090909091/100000000000 (= 6349.09090909091)\nwrapped to ~1.0326, producing a wrong-but-valid Real with n\n[…]\neserves the full\ni64 range. Negatives still work (covered by algebraic_tests' from_rational(-7,4)).\n\nAdds a regression test asserting a >i32 rational lowers exactly and not to the\nold truncated value.",
"is_bot": false,
"headline": "fix(Real): from_rational must not truncate i64 args to i32 (#568)",
"author_name": "Victor Heorhiadi",
"author_login": "progwriter",
"committed_at": "2026-06-26T17:33:47Z",
"body_truncated": true,
"is_coding_agent": false
},
{
"oid": "ef41610fd9eda689449d82b148e4827ad0c4f0c2",
"body": "…er. (#565)",
"is_bot": false,
"headline": "feat: Add bindings for `get_lower`/`get_upper` in the `Optimize` solv…",
"author_name": "Samuel Pastva",
"author_login": "daemontus",
"committed_at": "2026-06-22T11:10:37Z",
"body_truncated": false,
"is_coding_agent": false
},
{
"oid": "74c81a10e8d1524c70f8b14169d994d207bde939",
"body": null,
"is_bot": false,
"headline": "chore(z3): release v0.20.1 (#563)",
"author_name": "Mark DenHoed",
"author_login": "toolCHAINZ",
"committed_at": "2026-06-21T16:59:30Z",
"body_truncated": false,
"is_coding_agent": false
},
{
"oid": "0118a5e0a76a4e15227447548664ae1e160567bf",
"body": null,
"is_bot": false,
"headline": "enable \"num\" feature for z3 docs.rs build (#562)",
"author_name": "Alexander Coffin",
"author_login": "GreenBeard",
"committed_at": "2026-06-21T16:55:15Z",
"body_truncated": false,
"is_coding_agent": false
},
{
"oid": "7965d09c133f93c960694fd6b9cd6c51ad7e518b",
"body": null,
"is_bot": false,
"headline": "chore(z3-src): release v416.0.2 (#559)",
"author_name": "Mark DenHoed",
"author_login": "toolCHAINZ",
"committed_at": "2026-04-12T17:45:18Z",
"body_truncated": false,
"is_coding_agent": false
},
{
"oid": "3a03238cd30131c3a38cacbd3f8f6c15695d7e32",
"body": "Add z3-src to workspace members and update resolver.\nAdd a release-plz.toml package entry for z3-src with\nsemver_check = false. Make release-plz checkout fetch submodules.\nRemove the publish-z3-src GitHub Actions workflow and the\nPublishZ3Src/Z3SrcPatchPr xtask commands; update xtask output to\nadvise creating a PR so release-plz will publish on merge.",
"is_bot": false,
"headline": "chore: consolidate z3-src release process (#558)",
"author_name": "Mark DenHoed",
"author_login": "toolCHAINZ",
"committed_at": "2026-04-12T17:39:32Z",
"body_truncated": false,
"is_coding_agent": false
},
{
"oid": "ba1a853df48a93f1a6af07f049c2abb399ad86c9",
"body": "…ws (#557)",
"is_bot": false,
"headline": "fix: align MSVC runtime library to crt-static target feature on Windo…",
"author_name": "Kento",
"author_login": "kkent030315",
"committed_at": "2026-04-12T16:59:19Z",
"body_truncated": false,
"is_coding_agent": false
},
{
"oid": "c19dc55a1af4fd4b0590892f89f8e8f858292a2a",
"body": null,
"is_bot": false,
"headline": "chore: release (#528)",
"author_name": "Mark DenHoed",
"author_login": "toolCHAINZ",
"committed_at": "2026-04-01T18:31:14Z",
"body_truncated": false,
"is_coding_agent": false
},
{
"oid": "ced4149506948aaca0728d1abf71c2b53bf6f8a7",
"body": "… (#556)\n\n* chore: document minimum z3 version and feature gate optimize features\nfor now\n\n* fix conditionally-compiled tests\n\n* update readme title and z3 support table\n\n* Update README to clarify z3_4_16 feature flag status\n\nClarified that the feature flag for Optimize functions is temporary.",
"is_bot": false,
"headline": "chore: document minimum z3 version and feature gate optimize features…",
"author_name": "Mark DenHoed",
"author_login": "toolCHAINZ",
"committed_at": "2026-04-01T17:47:58Z",
"body_truncated": false,
"is_coding_agent": false
},
{
"oid": "75b88de3c2e9063a40cb62626f74cb9c0c0953ad",
"body": null,
"is_bot": false,
"headline": "chore: allow z3-src publish from branch",
"author_name": "Mark",
"author_login": "toolCHAINZ",
"committed_at": "2026-04-01T16:36:07Z",
"body_truncated": false,
"is_coding_agent": false
},
{
"oid": "1aed1a0dba0b49414ea3db3a16346fea6b9abcd7",
"body": "* cache tweaks\n\n* enable jobs on branch\n\n* remove flags\n\n* update wasm caching\n\n* trying stuff\n\n* test\n\n* update checkout to v6\n\n* bump actions/cache version\n\n* trying just using rust-cache\n\n* try cache-all-crates flag\n\n* restore sccache\n\n* just explicitly cache the windows z3-src build folder\n\n* Up\n[…]\nndows OS.\n\n* Uncomment conditional checks for master and tags\n\nAlso don't hash Cargo.lock because it breaks the cache constantly; will need to keep this in mind and occasionally clear the cache though",
"is_bot": false,
"headline": "chore: optimize CI and CI caching (#554)",
"author_name": "Mark DenHoed",
"author_login": "toolCHAINZ",
"committed_at": "2026-03-23T15:15:16Z",
"body_truncated": true,
"is_coding_agent": false
},
{
"oid": "fb844846391d74b0dfd6ca861ab7bd0b42769046",
"body": "* feat: add Char AST node and char sort\n\nIntroduce ast/char.rs with constructors (new_const, fresh_const,\nfrom_char, from_u32), conversions (to_string, to_int, to_bv, from_bv),\nand predicates/operators (is_digit, char_le). Export Char and impl\nDynamic::as_char in the ast module, and add Sort::char.\n\n* add simple unit tests\n\n* fmt\n\n* clippy",
"is_bot": false,
"headline": "feat: add Char Ast and Sort (#553)",
"author_name": "Mark DenHoed",
"author_login": "toolCHAINZ",
"committed_at": "2026-03-22T11:24:57Z",
"body_truncated": false,
"is_coding_agent": false
},
{
"oid": "a4fdb01d705942718f1c9b322e87ebd117f0c88c",
"body": null,
"is_bot": false,
"headline": "feat: make num dependency optional (#552)",
"author_name": "Mark DenHoed",
"author_login": "toolCHAINZ",
"committed_at": "2026-03-22T10:36:05Z",
"body_truncated": false,
"is_coding_agent": false
},
{
"oid": "426731446684e03639a52c8a4304e5037328c57f",
"body": null,
"is_bot": false,
"headline": "chore: fix workflow directory and metadata",
"author_name": "Mark",
"author_login": "toolCHAINZ",
"committed_at": "2026-03-21T18:24:02Z",
"body_truncated": false,
"is_coding_agent": false
},
{
"oid": "af6571acd84fd755c35032b410113b5de29bc196",
"body": null,
"is_bot": false,
"headline": "chore: release z3-src 416.0.1 (#551)",
"author_name": "Mark DenHoed",
"author_login": "toolCHAINZ",
"committed_at": "2026-03-21T18:16:53Z",
"body_truncated": false,
"is_coding_agent": false
},
{
"oid": "e4cea2ceb4ced2b0f0c65b68f22276c221d2d812",
"body": "* chore: add xtask command to create z3-src patch PR\n\n* fmt",
"is_bot": false,
"headline": "chore: add xtask command to create z3-src patch PR (#550)",
"author_name": "Mark DenHoed",
"author_login": "toolCHAINZ",
"committed_at": "2026-03-21T18:15:17Z",
"body_truncated": false,
"is_coding_agent": false
},
{
"oid": "074099e2a66d9d1b17289faece4732e86e037152",
"body": "* feat: Add Optimize::solutions\n\n* feat: Loosen Optimize::assert types\n\n* Fix clippy",
"is_bot": false,
"headline": "feat: Add Optimize::solutions and tweak Optimize::assert (#530)",
"author_name": "Mark DenHoed",
"author_login": "toolCHAINZ",
"committed_at": "2026-03-21T09:59:22Z",
"body_truncated": false,
"is_coding_agent": false
},
{
"oid": "bda4e53e9dbbbdf2176b8b22dc732a261e379917",
"body": "* feat: impl Translate and Clone for Optimize\n\n* add test\n\n* fmt\n\n* workflow tweak",
"is_bot": false,
"headline": "feat: impl Translate and Clone for Optimize (#529)",
"author_name": "Mark DenHoed",
"author_login": "toolCHAINZ",
"committed_at": "2026-03-21T09:33:25Z",
"body_truncated": false,
"is_coding_agent": false
},
{
"oid": "1c798bdac3466279d7c448cc5762f4f81b74a0ce",
"body": null,
"is_bot": false,
"headline": "Update release-plz.toml",
"author_name": "Mark",
"author_login": "toolCHAINZ",
"committed_at": "2026-03-20T23:45:40Z",
"body_truncated": false,
"is_coding_agent": false
},
{
"oid": "bea701a6e3c99d0564fedf31872f05b39a44713e",
"body": "* Add z3-src crate with add function and test\n\n* Add z3-src to workspace members\n\n* initial crate impl\n\n* Trim down included files\n\n* Remove build-time bindgen dependency: requires targeting specific z3\nversions now (which we already soft-required anyway)\n\n* check-in\n\n* Add generated Z3 bindings and\n[…]\n\n* Update z3-sys module docs\n\n* fmt build script\n\n* remove feature gates\n\n* Remove unused dependency\n\n* My search failed me\n\n* Remove outdated print\n\n* A couple doc tweaks\n\n* Update compatibility note",
"is_bot": false,
"headline": "feat!: add `vendored` build to pull z3 sources from crates.io (#510)",
"author_name": "Mark DenHoed",
"author_login": "toolCHAINZ",
"committed_at": "2026-03-20T23:43:12Z",
"body_truncated": true,
"is_coding_agent": false
},
{
"oid": "6d0853207b64aee8efd66c3e297b59f53ccbd5bc",
"body": null,
"is_bot": false,
"headline": "chore(z3): release v0.19.15 (#521)",
"author_name": "Mark DenHoed",
"author_login": "toolCHAINZ",
"committed_at": "2026-03-20T00:10:51Z",
"body_truncated": false,
"is_coding_agent": false
},
{
"oid": "e7f183c1b4588b74ee5f8ec7161b42bd75dc8b12",
"body": "…aints (#527)\n\n* Doc logical operators\n\n* doc pseudo-boolean constraints\n\n* Fix documentation formatting for atmost and atleast functions\n\nAdded missing backtics\n\n---------\n\nCo-authored-by: Mark DenHoed <mark.denhoed@cs.ox.ac.uk>",
"is_bot": false,
"headline": "doc: add missing docs for Boolean operators and pseudo-boolean constr…",
"author_name": "Matt Hofmann",
"author_login": "matth2k",
"committed_at": "2026-03-19T12:29:50Z",
"body_truncated": false,
"is_coding_agent": false
},
{
"oid": "2e0fd81faa59bc3da0550ff9c8c37af70725d26d",
"body": "…s (#526)\n\n* Annotate eval()\n\n* Const creation doc\n\n* atmost and ite doc\n\n* Int doc\n\n* Doc as_bool",
"is_bot": false,
"headline": "doc: add missing doc comments for Solver::eval() and several Ast impl…",
"author_name": "Matt Hofmann",
"author_login": "matth2k",
"committed_at": "2026-03-18T19:19:23Z",
"body_truncated": false,
"is_coding_agent": false
},
{
"oid": "cb655ca82388e3e45fce57a712914453c8b4149e",
"body": "* added: Optimize::get_assertions()\n\n* add small test\n\n* clippy",
"is_bot": false,
"headline": "added: Optimize::get_assertions (#523)",
"author_name": "Mark DenHoed",
"author_login": "toolCHAINZ",
"committed_at": "2026-03-16T17:05:29Z",
"body_truncated": false,
"is_coding_agent": false
},
{
"oid": "b83917b076f18125cadb909d92110eb1d8fe7dfb",
"body": "… (#522)",
"is_bot": false,
"headline": "fix: {Solver, Optimize}::check_and_get_model no longer take ownership…",
"author_name": "Mark DenHoed",
"author_login": "toolCHAINZ",
"committed_at": "2026-03-16T17:01:48Z",
"body_truncated": false,
"is_coding_agent": false
},
{
"oid": "0b330e361db8aa78fc3933a2ecda979735e5c40a",
"body": null,
"is_bot": false,
"headline": "feat: Implement Optimize Convenience Methods (#520)",
"author_name": "Mark DenHoed",
"author_login": "toolCHAINZ",
"committed_at": "2026-03-16T15:43:23Z",
"body_truncated": false,
"is_coding_agent": false
},
{
"oid": "c7244999a25ac3178f2d8c2e0abb046574d9a7a8",
"body": null,
"is_bot": false,
"headline": "chore: release (#516)",
"author_name": "Mark DenHoed",
"author_login": "toolCHAINZ",
"committed_at": "2026-03-13T10:29:16Z",
"body_truncated": false,
"is_coding_agent": false
},
{
"oid": "7b22690d42a994601fc43492335316d4a600802d",
"body": "* fix: use Sort::wrap instead of manually constructing it\n\n* slightly more cleanup\n\n* slightly more refactoring\n\n* more cleanup\n\n* further refactoring\n\n* add more tests\n\n* clippy\n\n* clippy\n\n* Remove rundundant docs, replace todo comment with assertion",
"is_bot": false,
"headline": "chore: internal refactoring of datatype builder (#517)",
"author_name": "Mark DenHoed",
"author_login": "toolCHAINZ",
"committed_at": "2026-03-13T10:23:52Z",
"body_truncated": false,
"is_coding_agent": false
},
{
"oid": "70e5dd396f55de899ddd9f4b0dc6786fc312804a",
"body": null,
"is_bot": false,
"headline": "Update zip dependency to latest (#515)",
"author_name": "Thomas Rooijakkers",
"author_login": "ThomasTNO",
"committed_at": "2026-03-12T13:25:37Z",
"body_truncated": false,
"is_coding_agent": false
},
{
"oid": "a189139b14228005cfe78cc4ca66f5bb95762cc7",
"body": null,
"is_bot": false,
"headline": "chore: release (#514)",
"author_name": "Mark DenHoed",
"author_login": "toolCHAINZ",
"committed_at": "2026-03-06T19:34:44Z",
"body_truncated": false,
"is_coding_agent": false
},
{
"oid": "e2e07018fb38a229c370ed6dcbb31ae40771b728",
"body": "CI builds can fail due to intermittent network slowdowns; a 30s timeout is too short.\nWe use Z3 in production builds and cannot assume it is present on every builder, so\nwe rely on the `gh-release` path and need it to be resilient to transient slowness.",
"is_bot": false,
"headline": "fix(z3-sys): raise GitHub download timeout for gh-release (#513)",
"author_name": "milevin",
"author_login": "milevin",
"committed_at": "2026-03-06T19:29:50Z",
"body_truncated": false,
"is_coding_agent": false
},
{
"oid": "65c7a6fbbb017c5e875645641ea7a487b14a72b8",
"body": null,
"is_bot": false,
"headline": "chore(z3): release v0.19.12 (#512)",
"author_name": "Mark DenHoed",
"author_login": "toolCHAINZ",
"committed_at": "2026-03-04T13:21:10Z",
"body_truncated": false,
"is_coding_agent": false
},
{
"oid": "aa5557bfa09ef2886b1c861d1e719c8e99400e66",
"body": null,
"is_bot": false,
"headline": "feat: add `with` method to Tactic (#511)",
"author_name": "longlinh123456",
"author_login": "longlinh123456",
"committed_at": "2026-03-04T12:21:26Z",
"body_truncated": false,
"is_coding_agent": false
},
{
"oid": "b532c1305836c800374d682fe19562d9d3f3f4e9",
"body": null,
"is_bot": false,
"headline": "chore(z3): release v0.19.11 (#507)",
"author_name": "Mark DenHoed",
"author_login": "toolCHAINZ",
"committed_at": "2026-02-27T09:02:49Z",
"body_truncated": false,
"is_coding_agent": false
},
{
"oid": "026cd51597890b23ecaf80711470fbdd8090e491",
"body": null,
"is_bot": false,
"headline": "added: FusedIterator and ExactSizeIterator for model/SortIter (#509)",
"author_name": "Mark DenHoed",
"author_login": "toolCHAINZ",
"committed_at": "2026-02-27T08:57:50Z",
"body_truncated": false,
"is_coding_agent": false
},
{
"oid": "582e1938e370492e16e489e8c6f40c3469fa3188",
"body": null,
"is_bot": false,
"headline": "fix: standardize AstVector display/debug impl (#508)",
"author_name": "Mark DenHoed",
"author_login": "toolCHAINZ",
"committed_at": "2026-02-27T08:47:34Z",
"body_truncated": false,
"is_coding_agent": false
},
{
"oid": "b18d4a6834f765278065ebace8c6b6743b1ab2de",
"body": null,
"is_bot": false,
"headline": "feat: add high-level API for model sorts/sort universes (#506)",
"author_name": "Mark DenHoed",
"author_login": "toolCHAINZ",
"committed_at": "2026-02-27T08:37:57Z",
"body_truncated": false,
"is_coding_agent": false
},
{
"oid": "97f57a99ac7057f38c6c8cdeac74f178ae2c2e7e",
"body": "* chore: release\n\n* Add @NikolajBjorner as contributor in changelogs",
"is_bot": false,
"headline": "chore: release (#503)",
"author_name": "Mark DenHoed",
"author_login": "toolCHAINZ",
"committed_at": "2026-02-24T10:09:06Z",
"body_truncated": false,
"is_coding_agent": false
},
{
"oid": "5631a0fd155e8babedf1cee4245a4d17cc5df7ae",
"body": null,
"is_bot": false,
"headline": "chore: bump Z3 default version to 4.16.0 (#504)",
"author_name": "Mark DenHoed",
"author_login": "toolCHAINZ",
"committed_at": "2026-02-24T10:00:54Z",
"body_truncated": false,
"is_coding_agent": false
},
{
"oid": "3d11d7449dad53a6327233909a3ca52ce9110f98",
"body": "…nd quantifier elimination (#500)\n\n* feat: Add Z3 API extensions - algebraic numbers, polynomials, enhanced floats, AST vectors, and quantifier elimination\n\n* Port existing ast_vector usages to the new high-level apis\n\n* Additional standard convenience impls for ast_vector and additional\nsimplificat\n[…]\nore doc tests\n\n* Add missing import comments to example code in docs\n\n* Allow passing None for rule name in fixedpoint add_rule API\n\n---------\n\nCo-authored-by: Nikolaj Bjorner <nbjorner@microsoft.com>",
"is_bot": false,
"headline": "feat: algebraic numbers, polynomials, enhanced floats, AST vectors, a…",
"author_name": "Mark DenHoed",
"author_login": "toolCHAINZ",
"committed_at": "2026-02-24T09:28:31Z",
"body_truncated": true,
"is_coding_agent": false
},
{
"oid": "f5640a3e2b0889740a666aca79757629a0b548ab",
"body": null,
"is_bot": false,
"headline": "chore: release (#497)",
"author_name": "Mark DenHoed",
"author_login": "toolCHAINZ",
"committed_at": "2026-02-21T20:32:36Z",
"body_truncated": false,
"is_coding_agent": false
},
{
"oid": "d9542b0b12114c5ced1df987feea494cbc210464",
"body": null,
"is_bot": false,
"headline": "chore: expand build flag documentation (#499)",
"author_name": "Mark DenHoed",
"author_login": "toolCHAINZ",
"committed_at": "2026-02-21T18:08:53Z",
"body_truncated": false,
"is_coding_agent": false
},
{
"oid": "ce50a037a210d2f12f8fdc63cb38e2445dfc7fef",
"body": "* fix: add rerun-if-env-changed for Z3_SYS_BUNDLED_DIR_OVERRIDE\n\nCloses #495\n\n* Make global const for Z3 override variable",
"is_bot": false,
"headline": "fix: add rerun-if-env-changed for Z3_SYS_BUNDLED_DIR_OVERRIDE (#496)",
"author_name": "Mark DenHoed",
"author_login": "toolCHAINZ",
"committed_at": "2026-02-14T08:33:12Z",
"body_truncated": false,
"is_coding_agent": false
},
{
"oid": "281c22f14cc12b314040799e12d64ed889cdc672",
"body": null,
"is_bot": false,
"headline": "chore: release (#492)",
"author_name": "Mark DenHoed",
"author_login": "toolCHAINZ",
"committed_at": "2026-02-13T12:41:45Z",
"body_truncated": false,
"is_coding_agent": false
},
{
"oid": "d5d112ddbcc1d55435a4dc9eb9af53d217495116",
"body": "Fixes #490\n\nZ3_SYS_BUNDLED_DIR_OVERRIDE includes a final 'z3' path fragment\nbut our construction of the header path also contains this fragment.\n\nThis change uses the correct path for overridden-builds while\nleaving the original behavior in place for non-overridden builds\nout of the OUT_DIR folder.",
"is_bot": false,
"headline": "fix: Z3_SYS_BUNDLED_DIR_OVERRIDE had extra z3 (#491)",
"author_name": "Mark DenHoed",
"author_login": "toolCHAINZ",
"committed_at": "2026-02-13T12:10:06Z",
"body_truncated": false,
"is_coding_agent": false
},
{
"oid": "11b153cdd4cf75af8d4ea2e47368f053b74603e4",
"body": null,
"is_bot": false,
"headline": "chore: release (#485)",
"author_name": "Mark DenHoed",
"author_login": "toolCHAINZ",
"committed_at": "2025-12-27T13:33:31Z",
"body_truncated": false,
"is_coding_agent": false
},
{
"oid": "b6b3f92716bb18c2478f7e6868c2d5f157203e56",
"body": "…#486)\n\n* feat: allow switching reqwest's tls provider\n\n* update docs\n\n* Bump default gh-release Z3 version",
"is_bot": false,
"headline": "feat: allow configuring tls provider for `gh-release` and `bundled` (…",
"author_name": "Mark DenHoed",
"author_login": "toolCHAINZ",
"committed_at": "2025-12-27T13:16:24Z",
"body_truncated": false,
"is_coding_agent": false
},
{
"oid": "b5d606409e10655f661e9f64415c2af01466c79d",
"body": null,
"is_bot": false,
"headline": "feat: Add check_and_get_model method to Solver (#484)",
"author_name": "Mark DenHoed",
"author_login": "toolCHAINZ",
"committed_at": "2025-12-27T12:32:01Z",
"body_truncated": false,
"is_coding_agent": false
},
{
"oid": "f518687de7ec40599ce489544bd246199f0fbe46",
"body": null,
"is_bot": false,
"headline": "chore(z3): release v0.19.6 (#480)",
"author_name": "Mark DenHoed",
"author_login": "toolCHAINZ",
"committed_at": "2025-12-10T17:43:33Z",
"body_truncated": false,
"is_coding_agent": false
},
{
"oid": "c3ca1672a0e7e0f62c6664dc3e19e16e18567bb7",
"body": "* feat: impl Sum and Product for Int and Real\n\n* fmt\n\n* clippy\n\n* fmt with newer rustfmt\n\n* Avoid extra term in sums/products at the cost of some refcounting",
"is_bot": false,
"headline": "feat: impl Sum and Product for Int and Real (#479)",
"author_name": "Mark DenHoed",
"author_login": "toolCHAINZ",
"committed_at": "2025-12-10T16:46:10Z",
"body_truncated": false,
"is_coding_agent": false
},
{
"oid": "2d8aa70b57d98be5fbf145b1da090ca3b99db4d5",
"body": null,
"is_bot": false,
"headline": "chore: release (#473)",
"author_name": "Mark DenHoed",
"author_login": "toolCHAINZ",
"committed_at": "2025-11-20T22:00:41Z",
"body_truncated": false,
"is_coding_agent": false
},
{
"oid": "dcf68bab47d7115a9c89f6217a3aefa2c295f3e4",
"body": "…macros (#471)\n\nuse absolute path to macro to avoid conditional import\n\nuse absolute path to IntoAst in trinop\n\nuse absolute path for macros in regexp for consistency",
"is_bot": false,
"headline": "refactor: remove unused imports in z3::ast and use absolute paths in …",
"author_name": "Felix Leitner",
"author_login": "lixitrixi",
"committed_at": "2025-11-20T21:09:27Z",
"body_truncated": false,
"is_coding_agent": false
},
{
"oid": "e958837a02222e59623b4477f2ce54b653453005",
"body": null,
"is_bot": false,
"headline": "feat: Use native-tls-vendored feature of reqwest dependency (#472)",
"author_name": "Erieke Weitenberg",
"author_login": "grebnetiew",
"committed_at": "2025-11-20T17:31:52Z",
"body_truncated": false,
"is_coding_agent": false
},
{
"oid": "a78da42f95bcb6fccdd2e96d474c3ac3f801a0d0",
"body": null,
"is_bot": false,
"headline": "chore: release (#469)",
"author_name": "Mark DenHoed",
"author_login": "toolCHAINZ",
"committed_at": "2025-11-18T00:03:16Z",
"body_truncated": false,
"is_coding_agent": false
},
{
"oid": "ed7f588f9c0da8d53de87318615c79fd9f5a7fba",
"body": null,
"is_bot": false,
"headline": "chore: bump bundled z3 (#470)",
"author_name": "Mark DenHoed",
"author_login": "toolCHAINZ",
"committed_at": "2025-11-17T23:39:32Z",
"body_truncated": false,
"is_coding_agent": false
},
{
"oid": "67303f6bc9dcf03e84f83d31955f730ea8239bbd",
"body": "* fix: use submodule for builds when it exists\n\n* fix\n\n* change prints\n\n* fmt\n\n* remove dbg",
"is_bot": false,
"headline": "fix: do not scrape GitHub when submodule exists (#468)",
"author_name": "Mark DenHoed",
"author_login": "toolCHAINZ",
"committed_at": "2025-11-17T23:25:13Z",
"body_truncated": false,
"is_coding_agent": false
},
{
"oid": "836bca2a01df6b5aead0762a461ecf8c02444183",
"body": null,
"is_bot": false,
"headline": "chore: release (#467)",
"author_name": "Mark DenHoed",
"author_login": "toolCHAINZ",
"committed_at": "2025-11-16T21:25:35Z",
"body_truncated": false,
"is_coding_agent": false
},
{
"oid": "e06259c0f49893637aafaeda4216b265fe8dc3e4",
"body": "…t (#464)\n\n* Implement support for bundling z3 without use of github checkout\n\n* Update README for bundled compilation instructions\n\n* Cargo fmt\n\n* Fix compilation issues",
"is_bot": false,
"headline": "feat: Implement support for bundling z3 without use of github checkou…",
"author_name": "Thomas Rooijakkers",
"author_login": "ThomasTNO",
"committed_at": "2025-11-16T20:31:15Z",
"body_truncated": false,
"is_coding_agent": false
},
{
"oid": "d23e8deed7e648e8deeb582be1cf9e39facfa323",
"body": null,
"is_bot": false,
"headline": "chore(z3): release v0.19.2 (#457)",
"author_name": "Mark DenHoed",
"author_login": "toolCHAINZ",
"committed_at": "2025-10-21T13:33:41Z",
"body_truncated": false,
"is_coding_agent": false
},
{
"oid": "0f6f9a2e5d4f6b3f89ff55e373c42d6ca9c29e39",
"body": "…nge` (#455)\n\nCo-authored-by: Mark DenHoed <mark.denhoed@cs.ox.ac.uk>",
"is_bot": false,
"headline": "feat: Add `Datatype::update_field`, `FuncDecl::domain`, `FuncDecl::ra…",
"author_name": "Will Crichton",
"author_login": "willcrichton",
"committed_at": "2025-10-21T12:13:16Z",
"body_truncated": false,
"is_coding_agent": false
},
{
"oid": "d89fdb61d47e29c3a5035a18258ab140b8965d84",
"body": "Appeasing clippy in rust 1.90",
"is_bot": false,
"headline": "feat: impl Default for Solver, Optimize, and Parser (#456)",
"author_name": "Mark DenHoed",
"author_login": "toolCHAINZ",
"committed_at": "2025-10-21T12:04:19Z",
"body_truncated": false,
"is_coding_agent": false
},
{
"oid": "f96c3b6a456b9f7bfd54df1c37759d28576617b4",
"body": null,
"is_bot": false,
"headline": "chore(z3): release v0.19.1 (#453)",
"author_name": "Mark DenHoed",
"author_login": "toolCHAINZ",
"committed_at": "2025-09-26T18:42:12Z",
"body_truncated": false,
"is_coding_agent": false
},
{
"oid": "ba32092148f42b59fc3c14d71a6acf3e744f85d1",
"body": null,
"is_bot": false,
"headline": "feat: allow context closures to capture non-Sync data (#452)",
"author_name": "Greg Morenz",
"author_login": "gmorenz",
"committed_at": "2025-09-26T18:39:41Z",
"body_truncated": false,
"is_coding_agent": false
},
{
"oid": "f222180ffaebbfce1801dfb230add3c72a19c80c",
"body": "* chore: release\n\n* Update versions\n\n* Update author",
"is_bot": false,
"headline": "chore: release (#446)",
"author_name": "Mark DenHoed",
"author_login": "toolCHAINZ",
"committed_at": "2025-09-26T11:49:11Z",
"body_truncated": false,
"is_coding_agent": false
},
{
"oid": "6617b868899cad2917c4073bcdfdeccd8b622e9f",
"body": "… private (#451)\n\n* removed: Context no longer implements Default and Context::new is now private\n\n* doc tweaks\n\n* doc tweaks\n\n* clippy",
"is_bot": false,
"headline": "removed: Context no longer implements Default and Context::new is now…",
"author_name": "Mark DenHoed",
"author_login": "toolCHAINZ",
"committed_at": "2025-09-26T11:13:35Z",
"body_truncated": false,
"is_coding_agent": false
},
{
"oid": "e1c1315fbe91be85831661526655ddff7002489c",
"body": "* Initial playing\n\n* porting things\n\n* build errors\n\n* test errors\n\n* tests fixed\n\n* fmt\n\n* macro docs and cleanup\n\n* some clippy\n\n* moar clippy\n\n* add a doc\n\n* fix doc test formatting\n\n* restore default ctx\n\n* macro simplification\n\n* Make the macro more idiomatic\n\n* merge master and fix tests\n\n* re\n[…]\nstions\n\n* Clippy\n\n* Use MaybeUninit::zeroed()\n\n* Clean up output params and high-level enum api\n\n* make placement of ? consistent\n\n* fmt\n\n* Represent output params as *mut *mut _Z3...\n\n* minimize diff",
"is_bot": false,
"headline": "changed: Fallible z3-sys APIs now return Option<NonNull<T>> (#450)",
"author_name": "Mark DenHoed",
"author_login": "toolCHAINZ",
"committed_at": "2025-09-26T10:21:11Z",
"body_truncated": true,
"is_coding_agent": false
},
{
"oid": "44618aeeda0538789f57ce5d7271e7abeca368be",
"body": null,
"is_bot": false,
"headline": "doc: fix typos in example (#448)",
"author_name": "Mark DenHoed",
"author_login": "toolCHAINZ",
"committed_at": "2025-09-11T21:34:24Z",
"body_truncated": false,
"is_coding_agent": false
},
{
"oid": "472e515c5a6d8890642301e84c50e75952ce3422",
"body": "* add: impl Translate for FuncDecl\n\n* fmt\n\n* Use z3 api for converting func_decl to ast\n\n* fmt\n\n* Use z3 api to convert back",
"is_bot": false,
"headline": "feat: impl Translate for FuncDecl (#439)",
"author_name": "Mark DenHoed",
"author_login": "toolCHAINZ",
"committed_at": "2025-09-11T09:19:44Z",
"body_truncated": false,
"is_coding_agent": false
},
{
"oid": "f8ae967ddd0423dcaf20484b874ce8931bcb4380",
"body": "* Add Order instantiation to FuncDecl\n\n* Formatting\n\n* Update func_decl.rs\n\n* Update func_decl.rs\n\n* Update func_decl.rs\n\n---------\n\nCo-authored-by: Mark DenHoed <mark.denhoed@cs.ox.ac.uk>",
"is_bot": false,
"headline": "feat: Special Binary Relation FuncDecls (#340)",
"author_name": "Samuel Grahn",
"author_login": "grahnen",
"committed_at": "2025-09-11T08:42:44Z",
"body_truncated": false,
"is_coding_agent": false
},
{
"oid": "3d9325a463ea8c8af1f1c19a947e0fc163d66f46",
"body": null,
"is_bot": false,
"headline": "chore(z3): release v0.18.2 (#445)",
"author_name": "Mark DenHoed",
"author_login": "toolCHAINZ",
"committed_at": "2025-09-10T14:16:49Z",
"body_truncated": false,
"is_coding_agent": false
},
{
"oid": "427e2d20444fe474e3476a98cfac8cf0c2f902b1",
"body": "* Try gating newer calls\n\n* A little more granular",
"is_bot": false,
"headline": "feat: gate newer Z3 APIs behind features (#444)",
"author_name": "Mark DenHoed",
"author_login": "toolCHAINZ",
"committed_at": "2025-09-10T14:13:57Z",
"body_truncated": false,
"is_coding_agent": false
},
{
"oid": "4f9db8ec8e3bd74c1e3cc1344e49cb185743f8df",
"body": null,
"is_bot": false,
"headline": "chore(z3): release v0.18.1 (#443)",
"author_name": "Mark DenHoed",
"author_login": "toolCHAINZ",
"committed_at": "2025-09-09T12:29:33Z",
"body_truncated": false,
"is_coding_agent": false
},
{
"oid": "19754a32ef20c40932d1fd14fe76df18754df435",
"body": "…(#442)\n\n* fix: Ast::ne -> Bool is now defined and used by the `ne` fn on all Ast types\n\n* Add a test\n\n* fmt",
"is_bot": false,
"headline": "fix: Ast::ne -> Bool is now defined and preferred over PartialEq::ne …",
"author_name": "Mark DenHoed",
"author_login": "toolCHAINZ",
"committed_at": "2025-09-09T12:26:49Z",
"body_truncated": false,
"is_coding_agent": false
},
{
"oid": "9d3fdc8f733eb22c1cf545735761dc32bb6a3a5a",
"body": null,
"is_bot": false,
"headline": "chore: release (#434)",
"author_name": "Mark DenHoed",
"author_login": "toolCHAINZ",
"committed_at": "2025-09-08T13:04:32Z",
"body_truncated": false,
"is_coding_agent": false
},
{
"oid": "bfe3f9b7a536db0b4a9833146ac6e2cfb5277e3f",
"body": "* fix: Solver::assert accepts `Borrow<Bool>` instead of `Into<Bool>`\n\n* fmt\n\n* Remove `From<bool> for Bool`",
"is_bot": false,
"headline": "changed!: APIs accepting `Bool` no longer accept `bool` (#436)",
"author_name": "Mark DenHoed",
"author_login": "toolCHAINZ",
"committed_at": "2025-09-08T12:58:03Z",
"body_truncated": false,
"is_coding_agent": false
},
{
"oid": "f7a75af333aec10e8118a105e5bde1084ae805b2",
"body": null,
"is_bot": false,
"headline": "doc: add simple example (#437)",
"author_name": "Mark DenHoed",
"author_login": "toolCHAINZ",
"committed_at": "2025-09-08T12:48:08Z",
"body_truncated": false,
"is_coding_agent": false
},
{
"oid": "183a4a33c06e0fc8b40527dc7ab94891c8a33f7b",
"body": "* fix: Solver::clone preserves tactics and params\n\n* doc",
"is_bot": false,
"headline": "fix: Solver::clone preserves tactics and params (#440)",
"author_name": "Mark DenHoed",
"author_login": "toolCHAINZ",
"committed_at": "2025-09-08T12:40:24Z",
"body_truncated": false,
"is_coding_agent": false
},
{
"oid": "8778c44b796188fe4a212b2effbe2e5f1ad70241",
"body": null,
"is_bot": false,
"headline": "Add nostd tags (#435)",
"author_name": "Mark DenHoed",
"author_login": "toolCHAINZ",
"committed_at": "2025-09-04T09:25:38Z",
"body_truncated": false,
"is_coding_agent": false
},
{
"oid": "66dcc18bf45448ca966de22be40271c5409af223",
"body": null,
"is_bot": false,
"headline": "feat: add consuming solutions iterator (#433)",
"author_name": "Mark DenHoed",
"author_login": "toolCHAINZ",
"committed_at": "2025-09-04T09:16:59Z",
"body_truncated": false,
"is_coding_agent": false
},
{
"oid": "63693cd6dd7540b287c9a817f772300c63281268",
"body": "* chore: release\n\n* Bump version and update changelog",
"is_bot": false,
"headline": "chore: release (#432)",
"author_name": "Mark DenHoed",
"author_login": "toolCHAINZ",
"committed_at": "2025-09-03T14:56:10Z",
"body_truncated": false,
"is_coding_agent": false
},
{
"oid": "46b763ca693c73e4d4bdd9dc2fd615d995a552b0",
"body": "* solver iterator stuff\n\n* doc tests and re-adding an `eq` to the Ast trait\n\n* add newline\n\n* Add 2-tuple and 3-tuple impls\n\n* doc tweak\n\n* Trait changes to allow implementing on slices and stuff\n\n* fmt\n\n* add doc comments for trait\n\n* Remove janky manual \"fuse\" logic and use the `fuse` adapter.",
"is_bot": false,
"headline": "feat: Add the ability to iterate over solutions from a `Solver` (#431)",
"author_name": "Mark DenHoed",
"author_login": "toolCHAINZ",
"committed_at": "2025-09-03T14:48:22Z",
"body_truncated": false,
"is_coding_agent": false
},
{
"oid": "41e9a0bdaeb41c83b452cce00aa80db305c2e598",
"body": "* Real fn renames and Eq refactor\n\nRename `_eq` to `eq` for consistency with `le`, `ge`, etc.\n\nRemove `PartialEq` and `Eq` from concrete `Ast` types to avoid accidental use.\n\nAdd `ast_eq` to `Ast` to allow for explicit ast equality checks.\n\nRename some `Real` methods involving fractions to \"rational\n[…]\nl\".\n\nExtend `Real::from_rational` (prev. `Real::from_real` to take `i64` for num/den).\n\n* eq fixes\n\n* merge tweaks and fixes\n\n* fmt + clippy\n\n---------\n\nCo-authored-by: Mark <mark.denhoed@cs.ox.ac.uk>",
"is_bot": false,
"headline": "changed: rename `_eq` to `eq` and `*_real_*` to `*_rational_*` (#305)",
"author_name": "Devin Jean",
"author_login": "dragazo",
"committed_at": "2025-09-03T08:52:24Z",
"body_truncated": true,
"is_coding_agent": false
},
{
"oid": "586dde24b348661e087c9edc508a1e01f1aadab9",
"body": "* changed: deprecate a couple now-useless Context APIs\n\n* Another deprecation\n\n* test fix",
"is_bot": false,
"headline": "changed: deprecate legacy Context APIs (#427)",
"author_name": "Mark DenHoed",
"author_login": "toolCHAINZ",
"committed_at": "2025-08-27T15:58:07Z",
"body_truncated": false,
"is_coding_agent": false
},
{
"oid": "310b3fe871df77bcd53fcfa2cf3f7e59f90763ab",
"body": null,
"is_bot": false,
"headline": "feat(z3-sys): do not depend on std (#425)",
"author_name": "lucascool12",
"author_login": "lucascool12",
"committed_at": "2025-08-27T09:30:03Z",
"body_truncated": false,
"is_coding_agent": false
},
{
"oid": "e94f1a728cd4ff8cd1a02b86088fdffec2aba49c",
"body": null,
"is_bot": false,
"headline": "chore: release (#424)",
"author_name": "Mark DenHoed",
"author_login": "toolCHAINZ",
"committed_at": "2025-08-25T22:17:38Z",
"body_truncated": false,
"is_coding_agent": false
},
{
"oid": "05087701175d39f81b7169d37965e2c535714023",
"body": null,
"is_bot": false,
"headline": "fix: use proper header path on overridden build (#423)",
"author_name": "Mark DenHoed",
"author_login": "toolCHAINZ",
"committed_at": "2025-08-25T22:15:06Z",
"body_truncated": false,
"is_coding_agent": false
},
{
"oid": "d87cee9161bac0b6b2c1f55652c1077ade9f7d71",
"body": null,
"is_bot": false,
"headline": "chore(z3): release v0.16.1 (#422)",
"author_name": "Mark DenHoed",
"author_login": "toolCHAINZ",
"committed_at": "2025-08-23T21:36:03Z",
"body_truncated": false,
"is_coding_agent": false
},
{
"oid": "608bb3361df0e833e58c3c2fb61c20d8f6294e9c",
"body": "…420)\n\n* A first pass at documenting how to define recursive datatypes\n\n* Smooth out API for making datatypes\n\n---------\n\nCo-authored-by: Mark <mark.denhoed@cs.ox.ac.uk>",
"is_bot": false,
"headline": "doc: A first pass at documenting how to define recursive datatypes (#…",
"author_name": "Patrick LaFontaine",
"author_login": "Pat-Lafon",
"committed_at": "2025-08-23T21:31:06Z",
"body_truncated": false,
"is_coding_agent": false
},
{
"oid": "43c28ad9f83e8e93e2b2158b0041e4b81966fd8a",
"body": "* chore(z3): release v0.16.0\n\n* Update Cargo.toml",
"is_bot": false,
"headline": "chore(z3): release v0.16.0 (#418)",
"author_name": "Mark DenHoed",
"author_login": "toolCHAINZ",
"committed_at": "2025-08-21T10:04:39Z",
"body_truncated": false,
"is_coding_agent": false
},
{
"oid": "257cee4928f177aa96a46f84ff5551f6362f47a2",
"body": null,
"is_bot": false,
"headline": "feat!: Use an implicit thread-local z3 context by default (#417)",
"author_name": "Mark DenHoed",
"author_login": "toolCHAINZ",
"committed_at": "2025-08-21T09:58:23Z",
"body_truncated": false,
"is_coding_agent": false
},
{
"oid": "83a094547cd89ea2f13f6000518d610c0a539776",
"body": null,
"is_bot": false,
"headline": "chore(z3): release v0.15.0 (#416)",
"author_name": "Mark DenHoed",
"author_login": "toolCHAINZ",
"committed_at": "2025-08-19T23:44:08Z",
"body_truncated": false,
"is_coding_agent": false
},
{
"oid": "9a0af8b46dc2782f789b11422716be92c531780a",
"body": "* added unit tests for round_towards_nearest_away/round_towards_nearest_even in tests/lib.rs\n\n* resolved merge conflict with the master\n\n* & removed in assert/ clippy",
"is_bot": false,
"headline": "chore: add unit tests for rounding modes (#389)",
"author_name": "Mehrad",
"author_login": "mehrad31415",
"committed_at": "2025-08-19T21:40:25Z",
"body_truncated": false,
"is_coding_agent": false
},
{
"oid": "ad6a95e15587e8d61bce9a9bfcdc6ce353906120",
"body": "This PR introduces the traits IntoAst and IntoAstFromCtx, which capture the ability of a type to be expressed in a Z3 ast, and changes the targets of most operations over all Ast types to take IntoAst<Self>. It additionally provides blanket implementations for existing Ast types and implementations \n[…]\n avoid the boilerplate of manually constructing trivial constants. Instead, you can use primitive rust types in most places you feel like you should be able to when building expressions: e.g. \"bv + 4\"",
"is_bot": false,
"headline": "feat!: trait-based conversions and operations (#410)",
"author_name": "Mark DenHoed",
"author_login": "toolCHAINZ",
"committed_at": "2025-08-19T10:42:18Z",
"body_truncated": true,
"is_coding_agent": false
},
{
"oid": "2174a51a189ff454307336d1bcfb56b89c760596",
"body": "* chore(z3): release v0.14.4\n\n* fix changelog",
"is_bot": false,
"headline": "chore: release (#415)",
"author_name": "Mark DenHoed",
"author_login": "toolCHAINZ",
"committed_at": "2025-08-19T09:07:09Z",
"body_truncated": false,
"is_coding_agent": false
}
],
"releases_count": 61,
"commits_last_year": 114,
"latest_release_at": "2026-07-23T11:42:00Z",
"latest_release_tag": "z3-sys-v0.12.0",
"releases_from_tags": false,
"days_since_last_push": 0,
"active_weeks_last_year": 25,
"days_since_latest_release": 0,
"mean_days_between_releases": 14.7
},
"community": {
"has_readme": true,
"has_license": false,
"has_description": true,
"has_contributing": false,
"health_percentage": 25,
"has_issue_template": false,
"has_code_of_conduct": false,
"has_pull_request_template": false
},
"ecosystem": {
"packages": [
{
"name": "z3",
"exists": true,
"license": "MIT",
"keywords": [
"ffi",
"solver",
"smt",
"satisfiability",
"api-bindings"
],
"ecosystem": "crates",
"matches_repo": true,
"registry_url": "https://crates.io/crates/z3",
"is_deprecated": false,
"latest_version": "0.20.2",
"repository_url": "https://github.com/prove-rs/z3.rs.git",
"versions_count": 55,
"total_downloads": 1471827,
"dependents_count": null,
"deprecation_note": null,
"maintainers_count": null,
"monthly_downloads": 164435,
"first_published_at": "2015-12-28T06:23:56.693379Z",
"latest_published_at": "2026-06-26T18:26:22.640344Z",
"latest_version_yanked": false,
"days_since_latest_publish": 26
},
{
"name": "xtask",
"exists": true,
"license": "MIT OR Apache-2.0",
"keywords": [
"automation",
"macos",
"release",
"codesign",
"xtask",
"command-line-utilities",
"development-tools::build-utils"
],
"ecosystem": "crates",
"matches_repo": false,
"registry_url": "https://crates.io/crates/xtask",
"is_deprecated": false,
"latest_version": "0.1.4",
"repository_url": "https://github.com/arcboxlabs/xtask",
"versions_count": 5,
"total_downloads": 554,
"dependents_count": null,
"deprecation_note": null,
"maintainers_count": null,
"monthly_downloads": 185,
"first_published_at": "2026-06-24T11:01:25.012607Z",
"latest_published_at": "2026-06-30T09:55:36.509458Z",
"latest_version_yanked": false,
"days_since_latest_publish": 23
},
{
"name": "z3-src",
"exists": true,
"license": "MIT",
"keywords": [
"solver",
"build",
"smt",
"satisfiability",
"development-tools::build-utils"
],
"ecosystem": "crates",
"matches_repo": true,
"registry_url": "https://crates.io/crates/z3-src",
"is_deprecated": false,
"latest_version": "500.0.0",
"repository_url": "https://github.com/prove-rs/z3.rs.git",
"versions_count": 10,
"total_downloads": 30287,
"dependents_count": null,
"deprecation_note": null,
"maintainers_count": null,
"monthly_downloads": 9492,
"first_published_at": "2026-02-24T13:20:33.907850Z",
"latest_published_at": "2026-07-22T19:00:02.081973Z",
"latest_version_yanked": false,
"days_since_latest_publish": 0
},
{
"name": "z3-sys",
"exists": true,
"license": "MIT",
"keywords": [
"ffi",
"solver",
"smt",
"satisfiability",
"no-std",
"external-ffi-bindings",
"no-std::no-alloc"
],
"ecosystem": "crates",
"matches_repo": true,
"registry_url": "https://crates.io/crates/z3-sys",
"is_deprecated": false,
"latest_version": "0.12.0",
"repository_url": "https://github.com/prove-rs/z3.rs.git",
"versions_count": 36,
"total_downloads": 1559630,
"dependents_count": null,
"deprecation_note": null,
"maintainers_count": null,
"monthly_downloads": 165755,
"first_published_at": "2015-12-28T02:31:50.656958Z",
"latest_published_at": "2026-07-23T11:41:56.210490Z",
"latest_version_yanked": false,
"days_since_latest_publish": 0
}
]
},
"popularity": {
"forks": 153,
"stars": 522,
"watchers": 6,
"fork_history": {
"days": [
{
"date": "2018-06-10",
"count": 1
},
{
"date": "2018-11-19",
"count": 1
},
{
"date": "2018-11-27",
"count": 1
},
{
"date": "2018-12-27",
"count": 1
},
{
"date": "2019-01-19",
"count": 1
},
{
"date": "2019-01-22",
"count": 1
},
{
"date": "2019-01-29",
"count": 1
},
{
"date": "2019-02-14",
"count": 1
},
{
"date": "2019-05-26",
"count": 1
},
{
"date": "2019-06-20",
"count": 1
},
{
"date": "2019-07-22",
"count": 1
},
{
"date": "2019-07-24",
"count": 1
},
{
"date": "2019-07-26",
"count": 1
},
{
"date": "2019-08-05",
"count": 1
},
{
"date": "2019-08-06",
"count": 1
},
{
"date": "2019-09-10",
"count": 1
},
{
"date": "2020-01-09",
"count": 1
},
{
"date": "2020-03-19",
"count": 1
},
{
"date": "2020-04-12",
"count": 1
},
{
"date": "2020-04-15",
"count": 1
},
{
"date": "2020-05-03",
"count": 1
},
{
"date": "2020-05-29",
"count": 1
},
{
"date": "2020-06-27",
"count": 1
},
{
"date": "2020-07-14",
"count": 1
},
{
"date": "2020-07-20",
"count": 1
},
{
"date": "2020-08-02",
"count": 1
},
{
"date": "2020-08-04",
"count": 1
},
{
"date": "2020-08-07",
"count": 1
},
{
"date": "2020-09-17",
"count": 1
},
{
"date": "2020-10-12",
"count": 1
},
{
"date": "2020-10-13",
"count": 1
},
{
"date": "2020-10-22",
"count": 1
},
{
"date": "2020-10-30",
"count": 1
},
{
"date": "2020-11-25",
"count": 1
},
{
"date": "2020-11-27",
"count": 1
},
{
"date": "2020-12-11",
"count": 1
},
{
"date": "2020-12-21",
"count": 1
},
{
"date": "2021-01-09",
"count": 1
},
{
"date": "2021-01-12",
"count": 1
},
{
"date": "2021-03-19",
"count": 1
},
{
"date": "2021-03-22",
"count": 1
},
{
"date": "2021-03-23",
"count": 1
},
{
"date": "2021-04-23",
"count": 1
},
{
"date": "2021-04-27",
"count": 1
},
{
"date": "2021-06-19",
"count": 1
},
{
"date": "2021-06-25",
"count": 1
},
{
"date": "2021-08-16",
"count": 1
},
{
"date": "2021-08-25",
"count": 1
},
{
"date": "2021-09-16",
"count": 1
},
{
"date": "2021-09-19",
"count": 1
},
{
"date": "2021-11-08",
"count": 1
},
{
"date": "2021-12-07",
"count": 1
},
{
"date": "2022-01-11",
"count": 1
},
{
"date": "2022-01-20",
"count": 1
},
{
"date": "2022-01-30",
"count": 1
},
{
"date": "2022-02-12",
"count": 1
},
{
"date": "2022-03-03",
"count": 1
},
{
"date": "2022-03-09",
"count": 1
},
{
"date": "2022-04-29",
"count": 1
},
{
"date": "2022-05-08",
"count": 1
},
{
"date": "2022-05-12",
"count": 1
},
{
"date": "2022-06-02",
"count": 1
},
{
"date": "2022-08-02",
"count": 1
},
{
"date": "2022-08-20",
"count": 1
},
{
"date": "2022-09-15",
"count": 1
},
{
"date": "2022-09-27",
"count": 1
},
{
"date": "2022-10-31",
"count": 1
},
{
"date": "2022-11-08",
"count": 1
},
{
"date": "2022-11-24",
"count": 1
},
{
"date": "2022-12-14",
"count": 2
},
{
"date": "2023-03-13",
"count": 1
},
{
"date": "2023-03-18",
"count": 1
},
{
"date": "2023-03-19",
"count": 1
},
{
"date": "2023-04-17",
"count": 1
},
{
"date": "2023-06-16",
"count": 1
},
{
"date": "2023-07-17",
"count": 1
},
{
"date": "2023-07-30",
"count": 1
},
{
"date": "2023-08-23",
"count": 1
},
{
"date": "2023-09-01",
"count": 1
},
{
"date": "2023-09-10",
"count": 1
},
{
"date": "2023-11-04",
"count": 1
},
{
"date": "2023-11-09",
"count": 1
},
{
"date": "2023-11-24",
"count": 1
},
{
"date": "2023-12-02",
"count": 1
},
{
"date": "2024-01-17",
"count": 1
},
{
"date": "2024-01-18",
"count": 1
},
{
"date": "2024-02-02",
"count": 1
},
{
"date": "2024-02-21",
"count": 1
},
{
"date": "2024-02-29",
"count": 1
},
{
"date": "2024-03-06",
"count": 1
},
{
"date": "2024-03-12",
"count": 1
},
{
"date": "2024-03-29",
"count": 1
},
{
"date": "2024-05-05",
"count": 1
},
{
"date": "2024-05-17",
"count": 1
},
{
"date": "2024-06-13",
"count": 1
},
{
"date": "2024-07-25",
"count": 1
},
{
"date": "2024-08-07",
"count": 1
},
{
"date": "2024-08-09",
"count": 2
},
{
"date": "2024-08-21",
"count": 1
},
{
"date": "2024-09-19",
"count": 1
},
{
"date": "2024-10-01",
"count": 1
},
{
"date": "2024-10-07",
"count": 1
},
{
"date": "2024-10-30",
"count": 1
},
{
"date": "2024-11-25",
"count": 1
},
{
"date": "2024-11-26",
"count": 1
},
{
"date": "2024-11-27",
"count": 1
},
{
"date": "2024-12-11",
"count": 1
},
{
"date": "2024-12-27",
"count": 1
},
{
"date": "2025-01-05",
"count": 1
},
{
"date": "2025-02-10",
"count": 1
},
{
"date": "2025-03-21",
"count": 1
},
{
"date": "2025-03-23",
"count": 1
},
{
"date": "2025-03-26",
"count": 1
},
{
"date": "2025-04-06",
"count": 1
},
{
"date": "2025-04-30",
"count": 1
},
{
"date": "2025-06-14",
"count": 1
},
{
"date": "2025-06-17",
"count": 1
},
{
"date": "2025-06-22",
"count": 1
},
{
"date": "2025-07-03",
"count": 1
},
{
"date": "2025-07-10",
"count": 1
},
{
"date": "2025-07-16",
"count": 1
},
{
"date": "2025-07-23",
"count": 2
},
{
"date": "2025-08-17",
"count": 1
},
{
"date": "2025-09-16",
"count": 1
},
{
"date": "2025-09-26",
"count": 1
},
{
"date": "2025-10-10",
"count": 1
},
{
"date": "2025-10-20",
"count": 1
},
{
"date": "2025-11-06",
"count": 1
},
{
"date": "2025-11-13",
"count": 1
},
{
"date": "2025-11-20",
"count": 3
},
{
"date": "2025-12-04",
"count": 2
},
{
"date": "2025-12-20",
"count": 1
},
{
"date": "2026-02-21",
"count": 1
},
{
"date": "2026-03-04",
"count": 1
},
{
"date": "2026-03-06",
"count": 1
},
{
"date": "2026-03-18",
"count": 1
},
{
"date": "2026-04-12",
"count": 1
},
{
"date": "2026-06-10",
"count": 1
},
{
"date": "2026-06-21",
"count": 1
},
{
"date": "2026-06-25",
"count": 1
},
{
"date": "2026-06-26",
"count": 1
},
{
"date": "2026-06-29",
"count": 1
}
],
"complete": true,
"collected": 148,
"total_forks": 153
},
"star_history": null,
"open_issues_and_prs": 48
},
"ai_readiness": {
"has_nix": false,
"example_dirs": [],
"has_llms_txt": false,
"has_dockerfile": false,
"has_mcp_signal": false,
"bootstrap_files": [],
"api_schema_files": [],
"has_devcontainer": false,
"typecheck_configs": [],
"toolchain_manifests": [
"Cargo.toml",
"xtask/Cargo.toml",
"z3-src/Cargo.toml",
"z3-sys/Cargo.toml",
"z3/Cargo.toml"
],
"largest_source_bytes": 56019,
"source_files_sampled": 64,
"oversized_source_files": 0,
"agent_instruction_files": [],
"agent_instruction_max_bytes": null
},
"dependencies": {
"manifests": [
"Cargo.toml",
"xtask/Cargo.toml",
"z3-src/Cargo.toml",
"z3-sys/Cargo.toml",
"z3/Cargo.toml"
],
"advisories": {
"error": null,
"scope": "published_package",
"source": "osv",
"findings": [],
"collected": true,
"malicious": [],
"truncated": false,
"by_severity": {},
"advisory_count": 0,
"affected_count": 0,
"assessed_count": 20,
"malicious_count": 0,
"assessed_package": "crates:z3@0.20.2",
"unassessed_count": 0,
"direct_affected_count": 0
},
"ecosystems": [
"crates"
],
"dependencies": [
{
"name": "clap",
"manifest": "xtask/Cargo.toml",
"ecosystem": "crates",
"version_constraint": "4.6"
},
{
"name": "semver",
"manifest": "xtask/Cargo.toml",
"ecosystem": "crates",
"version_constraint": "1"
},
{
"name": "cmake",
"manifest": "z3-src/Cargo.toml",
"ecosystem": "crates",
"version_constraint": "0.1.54"
},
{
"name": "log",
"manifest": "z3/Cargo.toml",
"ecosystem": "crates",
"version_constraint": "0.4"
},
{
"name": "num",
"manifest": "z3/Cargo.toml",
"ecosystem": "crates",
"version_constraint": "0.4"
},
{
"name": "z3-sys",
"manifest": "z3/Cargo.toml",
"ecosystem": "crates",
"version_constraint": "0.12.0"
}
],
"all_dependencies": {
"error": null,
"source": "github-sbom",
"packages": [
{
"name": "clap",
"direct": true,
"version": null,
"ecosystem": "crates"
},
{
"name": "cmake",
"direct": true,
"version": null,
"ecosystem": "crates"
},
{
"name": "log",
"direct": true,
"version": null,
"ecosystem": "crates"
},
{
"name": "num",
"direct": true,
"version": null,
"ecosystem": "crates"
},
{
"name": "semver",
"direct": true,
"version": null,
"ecosystem": "crates"
},
{
"name": "z3-sys",
"direct": true,
"version": null,
"ecosystem": "crates"
},
{
"name": "bindgen",
"direct": false,
"version": null,
"ecosystem": "crates"
},
{
"name": "env_logger",
"direct": false,
"version": null,
"ecosystem": "crates"
},
{
"name": "pkg-config",
"direct": false,
"version": null,
"ecosystem": "crates"
},
{
"name": "prettyplease",
"direct": false,
"version": null,
"ecosystem": "crates"
},
{
"name": "proc-macro2",
"direct": false,
"version": null,
"ecosystem": "crates"
},
{
"name": "quote",
"direct": false,
"version": null,
"ecosystem": "crates"
},
{
"name": "rayon",
"direct": false,
"version": null,
"ecosystem": "crates"
},
{
"name": "regex",
"direct": false,
"version": null,
"ecosystem": "crates"
},
{
"name": "reqwest",
"direct": false,
"version": null,
"ecosystem": "crates"
},
{
"name": "serde_json",
"direct": false,
"version": null,
"ecosystem": "crates"
},
{
"name": "syn",
"direct": false,
"version": null,
"ecosystem": "crates"
},
{
"name": "vcpkg",
"direct": false,
"version": null,
"ecosystem": "crates"
},
{
"name": "z3-src",
"direct": false,
"version": null,
"ecosystem": "crates"
},
{
"name": "zip",
"direct": false,
"version": null,
"ecosystem": "crates"
}
],
"collected": true,
"truncated": false,
"total_count": 20,
"direct_count": 6,
"indirect_count": 14
}
},
"maintainership": {
"issues": {
"open_prs": 11,
"merged_prs": 328,
"open_issues": 37,
"closed_ratio": 0.797,
"closed_issues": 145,
"closed_unmerged_prs": 39
},
"bus_factor": 3,
"bot_contributors": 0,
"top_contributors": [
{
"type": "User",
"login": "waywardmonkeys",
"commits": 200,
"avatar_url": "https://avatars.githubusercontent.com/u/178582?v=4"
},
{
"type": "User",
"login": "toolCHAINZ",
"commits": 122,
"avatar_url": "https://avatars.githubusercontent.com/u/27028960?v=4"
},
{
"type": "User",
"login": "fitzgen",
"commits": 75,
"avatar_url": "https://avatars.githubusercontent.com/u/74571?v=4"
},
{
"type": "User",
"login": "Pat-Lafon",
"commits": 26,
"avatar_url": "https://avatars.githubusercontent.com/u/32135464?v=4"
},
{
"type": "User",
"login": "sameer",
"commits": 24,
"avatar_url": "https://avatars.githubusercontent.com/u/11097096?v=4"
},
{
"type": "User",
"login": "juliusrakow",
"commits": 23,
"avatar_url": "https://avatars.githubusercontent.com/u/253821909?v=4"
},
{
"type": "User",
"login": "SeeSpring",
"commits": 18,
"avatar_url": "https://avatars.githubusercontent.com/u/30735327?v=4"
},
{
"type": "User",
"login": "rlkelly",
"commits": 12,
"avatar_url": "https://avatars.githubusercontent.com/u/4022974?v=4"
},
{
"type": "User",
"login": "cdisselkoen",
"commits": 11,
"avatar_url": "https://avatars.githubusercontent.com/u/4458638?v=4"
},
{
"type": "User",
"login": "taegyunkim",
"commits": 11,
"avatar_url": "https://avatars.githubusercontent.com/u/6655247?v=4"
}
],
"contributors_sampled": 78,
"top_contributor_share": 0.309
},
"quality_signals": {
"has_ci": true,
"has_tests": true,
"ci_workflows": [
"release-plz.yml",
"release-z3-src.yml",
"rust.yml"
],
"has_docs_dir": false,
"linter_configs": [],
"has_editorconfig": false,
"has_linter_config": false,
"has_precommit_config": false
},
"security_signals": {
"lockfiles": [],
"scorecard": {
"checks": [
{
"name": "Binary-Artifacts",
"score": 10,
"reason": "no binaries found in the repo",
"documentation_url": "https://github.com/ossf/scorecard/blob/c395761df6afe1a69e476bc60a013a94bcbc153f/docs/checks.md#binary-artifacts"
},
{
"name": "Branch-Protection",
"score": 0,
"reason": "branch protection not enabled on development/release branches",
"documentation_url": "https://github.com/ossf/scorecard/blob/c395761df6afe1a69e476bc60a013a94bcbc153f/docs/checks.md#branch-protection"
},
{
"name": "CI-Tests",
"score": 9,
"reason": "25 out of 27 merged PRs checked by a CI test -- score normalized to 9",
"documentation_url": "https://github.com/ossf/scorecard/blob/c395761df6afe1a69e476bc60a013a94bcbc153f/docs/checks.md#ci-tests"
},
{
"name": "CII-Best-Practices",
"score": 0,
"reason": "no effort to earn an OpenSSF best practices badge detected",
"documentation_url": "https://github.com/ossf/scorecard/blob/c395761df6afe1a69e476bc60a013a94bcbc153f/docs/checks.md#cii-best-practices"
},
{
"name": "Code-Review",
"score": 2,
"reason": "Found 6/30 approved changesets -- score normalized to 2",
"documentation_url": "https://github.com/ossf/scorecard/blob/c395761df6afe1a69e476bc60a013a94bcbc153f/docs/checks.md#code-review"
},
{
"name": "Contributors",
"score": 10,
"reason": "project has 26 contributing companies or organizations",
"documentation_url": "https://github.com/ossf/scorecard/blob/c395761df6afe1a69e476bc60a013a94bcbc153f/docs/checks.md#contributors"
},
{
"name": "Dangerous-Workflow",
"score": 10,
"reason": "no dangerous workflow patterns detected",
"documentation_url": "https://github.com/ossf/scorecard/blob/c395761df6afe1a69e476bc60a013a94bcbc153f/docs/checks.md#dangerous-workflow"
},
{
"name": "Dependency-Update-Tool",
"score": 0,
"reason": "no update tool detected",
"documentation_url": "https://github.com/ossf/scorecard/blob/c395761df6afe1a69e476bc60a013a94bcbc153f/docs/checks.md#dependency-update-tool"
},
{
"name": "Fuzzing",
"score": 0,
"reason": "project is not fuzzed",
"documentation_url": "https://github.com/ossf/scorecard/blob/c395761df6afe1a69e476bc60a013a94bcbc153f/docs/checks.md#fuzzing"
},
{
"name": "License",
"score": 0,
"reason": "license file not detected",
"documentation_url": "https://github.com/ossf/scorecard/blob/c395761df6afe1a69e476bc60a013a94bcbc153f/docs/checks.md#license"
},
{
"name": "Maintained",
"score": 10,
"reason": "10 commit(s) and 4 issue activity found in the last 90 days -- score normalized to 10",
"documentation_url": "https://github.com/ossf/scorecard/blob/c395761df6afe1a69e476bc60a013a94bcbc153f/docs/checks.md#maintained"
},
{
"name": "Packaging",
"score": null,
"reason": "packaging workflow not detected",
"documentation_url": "https://github.com/ossf/scorecard/blob/c395761df6afe1a69e476bc60a013a94bcbc153f/docs/checks.md#packaging"
},
{
"name": "Pinned-Dependencies",
"score": 0,
"reason": "dependency not pinned by hash detected -- score normalized to 0",
"documentation_url": "https://github.com/ossf/scorecard/blob/c395761df6afe1a69e476bc60a013a94bcbc153f/docs/checks.md#pinned-dependencies"
},
{
"name": "SAST",
"score": 0,
"reason": "SAST tool is not run on all commits -- score normalized to 0",
"documentation_url": "https://github.com/ossf/scorecard/blob/c395761df6afe1a69e476bc60a013a94bcbc153f/docs/checks.md#sast"
},
{
"name": "Security-Policy",
"score": 0,
"reason": "security policy file not detected",
"documentation_url": "https://github.com/ossf/scorecard/blob/c395761df6afe1a69e476bc60a013a94bcbc153f/docs/checks.md#security-policy"
},
{
"name": "Signed-Releases",
"score": null,
"reason": "no releases found",
"documentation_url": "https://github.com/ossf/scorecard/blob/c395761df6afe1a69e476bc60a013a94bcbc153f/docs/checks.md#signed-releases"
},
{
"name": "Token-Permissions",
"score": 0,
"reason": "detected GitHub workflow tokens with excessive permissions",
"documentation_url": "https://github.com/ossf/scorecard/blob/c395761df6afe1a69e476bc60a013a94bcbc153f/docs/checks.md#token-permissions"
},
{
"name": "Vulnerabilities",
"score": 10,
"reason": "0 existing vulnerabilities detected",
"documentation_url": "https://github.com/ossf/scorecard/blob/c395761df6afe1a69e476bc60a013a94bcbc153f/docs/checks.md#vulnerabilities"
}
],
"commit": "e717cdd1275333e6b3529b60b8d12d12ab121853",
"ran_at": "2026-07-23T15:28:34Z",
"aggregate_score": 4.2,
"scorecard_version": "v5.5.0"
},
"has_codeql_workflow": false,
"has_security_policy": false,
"has_dependabot_config": false
},
"contribution_flow": {
"collected": true,
"ci_last_run_at": "2026-07-23T12:23:54Z",
"oldest_open_prs": [
{
"number": 264,
"created_at": "2023-10-29T10:46:10Z",
"last_comment_at": "2023-10-29T13:25:53Z",
"last_comment_author": "TheVeryDarkness"
},
{
"number": 306,
"created_at": "2024-08-02T10:59:06Z",
"last_comment_at": "2024-08-02T17:16:43Z",
"last_comment_author": "dragazo"
},
{
"number": 307,
"created_at": "2024-08-02T10:59:26Z",
"last_comment_at": null,
"last_comment_author": null
},
{
"number": 314,
"created_at": "2024-10-08T18:35:40Z",
"last_comment_at": "2025-09-16T22:46:00Z",
"last_comment_author": "toolCHAINZ"
},
{
"number": 330,
"created_at": "2024-12-11T22:10:28Z",
"last_comment_at": null,
"last_comment_author": null
},
{
"number": 344,
"created_at": "2025-04-08T13:30:56Z",
"last_comment_at": "2026-02-23T20:50:13Z",
"last_comment_author": "puyral"
},
{
"number": 383,
"created_at": "2025-07-22T01:13:13Z",
"last_comment_at": "2025-07-22T11:01:34Z",
"last_comment_author": "toolCHAINZ"
},
{
"number": 387,
"created_at": "2025-07-25T05:46:19Z",
"last_comment_at": "2025-08-19T09:02:24Z",
"last_comment_author": "toolCHAINZ"
},
{
"number": 462,
"created_at": "2025-11-06T21:38:43Z",
"last_comment_at": null,
"last_comment_author": null
},
{
"number": 567,
"created_at": "2026-06-22T13:08:01Z",
"last_comment_at": "2026-06-24T15:10:03Z",
"last_comment_author": "daemontus"
},
{
"number": 574,
"created_at": "2026-07-23T11:41:51Z",
"last_comment_at": "2026-07-23T11:52:19Z",
"last_comment_author": "toolCHAINZ"
}
],
"last_merged_pr_at": "2026-07-23T11:46:15Z",
"ci_last_conclusion": "SUCCESS",
"oldest_open_issues": [
{
"number": 149,
"created_at": "2021-07-07T03:37:02Z",
"last_comment_at": "2026-06-10T16:00:47Z",
"last_comment_author": "DavidEichmann"
},
{
"number": 151,
"created_at": "2021-07-20T05:51:25Z",
"last_comment_at": "2025-09-15T14:07:34Z",
"last_comment_author": "asibahi"
},
{
"number": 162,
"created_at": "2021-09-28T05:15:48Z",
"last_comment_at": "2025-09-02T00:13:17Z",
"last_comment_author": "toolCHAINZ"
},
{
"number": 189,
"created_at": "2022-03-18T04:24:17Z",
"last_comment_at": null,
"last_comment_author": null
},
{
"number": 238,
"created_at": "2023-05-02T17:41:17Z",
"last_comment_at": "2023-05-03T11:41:12Z",
"last_comment_author": "dp1"
},
{
"number": 343,
"created_at": "2025-04-06T07:55:59Z",
"last_comment_at": "2025-04-07T15:22:16Z",
"last_comment_author": "Pat-Lafon"
},
{
"number": 351,
"created_at": "2025-06-20T14:50:10Z",
"last_comment_at": "2025-09-28T16:26:15Z",
"last_comment_author": "toolCHAINZ"
},
{
"number": 421,
"created_at": "2025-08-23T21:15:54Z",
"last_comment_at": "2025-09-06T21:29:14Z",
"last_comment_author": "toolCHAINZ"
},
{
"number": 447,
"created_at": "2025-09-11T09:48:33Z",
"last_comment_at": "2025-09-11T22:05:46Z",
"last_comment_author": "toolCHAINZ"
},
{
"number": 458,
"created_at": "2025-10-30T16:56:23Z",
"last_comment_at": "2025-11-05T00:14:33Z",
"last_comment_author": "toolCHAINZ"
},
{
"number": 460,
"created_at": "2025-11-06T11:24:51Z",
"last_comment_at": "2025-11-07T10:00:02Z",
"last_comment_author": "toolCHAINZ"
},
{
"number": 461,
"created_at": "2025-11-06T11:28:20Z",
"last_comment_at": null,
"last_comment_author": null
},
{
"number": 463,
"created_at": "2025-11-12T22:43:12Z",
"last_comment_at": "2026-03-21T10:50:36Z",
"last_comment_author": "toolCHAINZ"
},
{
"number": 476,
"created_at": "2025-11-29T11:32:18Z",
"last_comment_at": "2025-12-27T13:51:44Z",
"last_comment_author": "lixitrixi"
},
{
"number": 483,
"created_at": "2025-12-27T09:12:12Z",
"last_comment_at": "2026-04-27T13:53:42Z",
"last_comment_author": "gskorokhod"
},
{
"number": 489,
"created_at": "2026-01-31T16:49:34Z",
"last_comment_at": "2026-01-31T19:22:38Z",
"last_comment_author": "toolCHAINZ"
},
{
"number": 501,
"created_at": "2026-02-23T14:59:07Z",
"last_comment_at": "2026-02-24T17:09:26Z",
"last_comment_author": "niooii"
},
{
"number": 532,
"created_at": "2026-03-21T12:00:31Z",
"last_comment_at": null,
"last_comment_author": null
},
{
"number": 533,
"created_at": "2026-03-21T12:01:36Z",
"last_comment_at": "2026-03-23T15:38:47Z",
"last_comment_author": "toolCHAINZ"
},
{
"number": 534,
"created_at": "2026-03-21T12:02:52Z",
"last_comment_at": null,
"last_comment_author": null
}
]
}
},
"config": {
"disabled_metrics": [],
"disabled_categories": [],
"disabled_components": {}
},
"source": {
"url": "https://github.com/prove-rs/z3.rs",
"host": "github.com",
"name": "z3.rs",
"owner": "prove-rs"
},
"metrics": {
"overall": {
"key": "overall",
"band": "moderate",
"name": "Overall health",
"note": null,
"notes": [],
"value": 69,
"inputs": {
"security": 54,
"vitality": 89,
"community": 58,
"governance": 74,
"engineering": 64
},
"components": []
},
"categories": [
{
"key": "vitality",
"band": "excellent",
"name": "Vitality",
"value": 89,
"weight": 0.22,
"metrics": [
{
"key": "development_activity",
"band": "good",
"name": "Development activity",
"note": null,
"notes": [],
"value": 81,
"inputs": {
"commits_last_year": 114,
"human_commit_share": 1,
"days_since_last_push": 0,
"active_weeks_last_year": 25
},
"components": [
{
"key": "push_recency",
"name": "Push recency",
"detail": "last push 0 days ago",
"points": 36,
"status": "met",
"details": [
{
"code": "push_recency",
"params": {
"days": 0
}
}
],
"max_points": 36
},
{
"key": "commit_cadence",
"name": "Commit cadence",
"detail": "25/52 weeks with commits",
"points": 17.3,
"status": "partial",
"details": [
{
"code": "commit_cadence_weeks",
"params": {
"weeks": 25
}
}
],
"max_points": 36
},
{
"key": "commit_volume",
"name": "Commit volume",
"detail": "114 commits in the last year",
"points": 18,
"status": "met",
"details": [
{
"code": "commits_last_year",
"params": {
"count": 114
}
}
],
"max_points": 18
},
{
"key": "openssf_scorecard_maintained",
"name": "OpenSSF Scorecard: Maintained",
"detail": "10 commit(s) and 4 issue activity found in the last 90 days -- score normalized to 10",
"points": 10,
"status": "met",
"details": [],
"max_points": 10
}
]
},
{
"key": "release_discipline",
"band": "excellent",
"name": "Release discipline",
"note": "Excluded from scoring (no data or not applicable): OpenSSF Scorecard: Signed-Releases. Remaining weights renormalized.",
"notes": [
{
"code": "excluded_no_data",
"params": {
"components": [
"openssf_scorecard_signed_releases"
]
}
},
{
"code": "weights_renormalized",
"params": {}
}
],
"value": 100,
"inputs": {
"releases_count": 61,
"latest_release_tag": "z3-sys-v0.12.0",
"releases_from_tags": false,
"days_since_latest_release": 0,
"mean_days_between_releases": 14.7
},
"components": [
{
"key": "ships_releases",
"name": "Ships releases",
"detail": "61 releases published",
"points": 27,
"status": "met",
"details": [
{
"code": "releases_published",
"params": {
"count": 61
}
}
],
"max_points": 27
},
{
"key": "release_recency",
"name": "Release recency",
"detail": "latest release 0 days ago",
"points": 36,
"status": "met",
"details": [
{
"code": "release_recency",
"params": {
"days": 0
}
}
],
"max_points": 36
},
{
"key": "release_cadence",
"name": "Release cadence",
"detail": "a release every ~14.7 days",
"points": 27,
"status": "met",
"details": [
{
"code": "release_cadence",
"params": {
"gap": 14.7
}
}
],
"max_points": 27
},
{
"key": "openssf_scorecard_signed_releases",
"name": "OpenSSF Scorecard: Signed-Releases",
"detail": "no releases found",
"points": 0,
"status": "excluded",
"details": [
{
"code": "no_data",
"params": {}
}
],
"max_points": 10
}
]
},
{
"key": "abandonment",
"band": "excellent",
"name": "Abandonment",
"note": null,
"notes": [],
"value": 100,
"inputs": {
"cap": null,
"state": "maintained",
"guards": [],
"signals": [],
"red_flag": false,
"multiplier_pct": 100,
"declared_reason": null,
"unverified_reason": null,
"unanswered_open_prs": null,
"unanswered_open_issues": null,
"days_since_last_merged_pr": null,
"days_since_last_human_commit": 0,
"days_since_last_human_commit_is_floor": false
},
"components": [
{
"key": "project_is_still_maintained",
"name": "Project is still maintained",
"detail": "last human commit 0 days ago",
"points": 100,
"status": "met",
"details": [
{
"code": "abandonment_maintained",
"params": {
"days": 0
}
}
],
"max_points": 100
}
]
}
],
"description": "Is the project alive — is code being written and are releases shipping?"
},
{
"key": "community",
"band": "moderate",
"name": "Community & Adoption",
"value": 58,
"weight": 0.18,
"metrics": [
{
"key": "popularity",
"band": "moderate",
"name": "Popularity & adoption",
"note": null,
"notes": [],
"value": 66,
"inputs": {
"forks": 153,
"stars": 522,
"watchers": 6,
"growth_state": "unverified",
"growth_factor_pct": 100,
"growth_unverified_reason": "no_history"
},
"components": [
{
"key": "stars",
"name": "Stars",
"detail": "522 stars",
"points": 44.1,
"status": "partial",
"details": [
{
"code": "stars",
"params": {
"count": 522
}
}
],
"max_points": 60
},
{
"key": "forks",
"name": "Forks",
"detail": "153 forks",
"points": 18.2,
"status": "partial",
"details": [
{
"code": "forks",
"params": {
"count": 153
}
}
],
"max_points": 25
},
{
"key": "watchers",
"name": "Watchers",
"detail": "6 watchers",
"points": 3.9,
"status": "partial",
"details": [
{
"code": "watchers",
"params": {
"count": 6
}
}
],
"max_points": 15
}
]
},
{
"key": "community_health",
"band": "critical",
"name": "Community health",
"note": null,
"notes": [],
"value": 25,
"inputs": {
"has_readme": true,
"has_license": false,
"has_contributing": false,
"has_issue_template": false,
"has_code_of_conduct": false,
"has_pull_request_template": false
},
"components": [
{
"key": "readme",
"name": "README",
"detail": null,
"points": 22.5,
"status": "met",
"details": [],
"max_points": 22.5
},
{
"key": "license",
"name": "License",
"detail": "no license file detected",
"points": 0,
"status": "missed",
"details": [
{
"code": "license_absent",
"params": {}
}
],
"max_points": 22.5
},
{
"key": "contributing_guide",
"name": "CONTRIBUTING guide",
"detail": null,
"points": 0,
"status": "missed",
"details": [],
"max_points": 18
},
{
"key": "code_of_conduct",
"name": "Code of conduct",
"detail": null,
"points": 0,
"status": "missed",
"details": [],
"max_points": 13.5
},
{
"key": "issue_template",
"name": "Issue template",
"detail": null,
"points": 0,
"status": "missed",
"details": [],
"max_points": 7.2
},
{
"key": "pr_template",
"name": "PR template",
"detail": null,
"points": 0,
"status": "missed",
"details": [],
"max_points": 6.3
}
]
},
{
"key": "ecosystem_adoption",
"band": "excellent",
"name": "Ecosystem adoption (downloads)",
"note": "Excluded from scoring (no data or not applicable): Registry dependents. Remaining weights renormalized.",
"notes": [
{
"code": "excluded_no_data",
"params": {
"components": [
"registry_dependents"
]
}
},
{
"code": "weights_renormalized",
"params": {}
}
],
"value": 92,
"inputs": {
"packages": [
"z3",
"z3-src",
"z3-sys"
],
"dependents": null,
"ecosystems": "crates",
"total_downloads": 3061744,
"monthly_downloads": 339682
},
"components": [
{
"key": "monthly_downloads",
"name": "Monthly downloads",
"detail": "339,682 downloads/month across crates",
"points": 73.7,
"status": "partial",
"details": [
{
"code": "downloads_monthly",
"params": {
"count": 339682,
"ecosystems": "crates"
}
}
],
"max_points": 80
},
{
"key": "registry_dependents",
"name": "Registry dependents",
"detail": "not reported by this ecosystem",
"points": 0,
"status": "excluded",
"details": [
{
"code": "not_reported_by_this_ecosystem",
"params": {}
}
],
"max_points": 20
}
]
}
],
"description": "Does the project have users, downloads, attention, and a welcoming setup for contributors?"
},
{
"key": "governance",
"band": "good",
"name": "Sustainability & Governance",
"value": 74,
"weight": 0.24,
"metrics": [
{
"key": "maintainer_resilience",
"band": "good",
"name": "Maintainer resilience (bus factor)",
"note": null,
"notes": [],
"value": 75,
"inputs": {
"bus_factor": 3,
"contributors_sampled": 78,
"top_contributor_share": 0.309
},
"components": [
{
"key": "bus_factor",
"name": "Bus factor",
"detail": "3 contributor(s) cover half of all commits",
"points": 36,
"status": "partial",
"details": [
{
"code": "bus_factor",
"params": {
"count": 3
}
}
],
"max_points": 54
},
{
"key": "commit_distribution",
"name": "Commit distribution",
"detail": "top contributor authored 31% of commits",
"points": 15.5,
"status": "partial",
"details": [
{
"code": "top_contributor_share",
"params": {
"share": 31
}
}
],
"max_points": 22.5
},
{
"key": "contributor_breadth",
"name": "Contributor breadth",
"detail": "78 contributors",
"points": 13.5,
"status": "met",
"details": [
{
"code": "contributors_sampled",
"params": {
"count": 78
}
}
],
"max_points": 13.5
},
{
"key": "openssf_scorecard_contributors",
"name": "OpenSSF Scorecard: Contributors",
"detail": "project has 26 contributing companies or organizations",
"points": 10,
"status": "met",
"details": [],
"max_points": 10
}
]
},
{
"key": "responsiveness",
"band": "good",
"name": "Issue & PR responsiveness",
"note": null,
"notes": [],
"value": 74,
"inputs": {
"merged_prs": 328,
"open_issues": 37,
"closed_issues": 145,
"issue_closed_ratio": 0.797,
"closed_unmerged_prs": 39
},
"components": [
{
"key": "issue_resolution",
"name": "Issue resolution",
"detail": "80% of issues closed",
"points": 37.3,
"status": "partial",
"details": [
{
"code": "issues_closed_share",
"params": {
"share": 80
}
}
],
"max_points": 46.75
},
{
"key": "pr_acceptance",
"name": "PR acceptance",
"detail": "328/367 decided PRs merged",
"points": 34.2,
"status": "partial",
"details": [
{
"code": "decided_prs_merged",
"params": {
"merged": 328,
"decided": 367
}
}
],
"max_points": 38.25
},
{
"key": "openssf_scorecard_code_review",
"name": "OpenSSF Scorecard: Code-Review",
"detail": "Found 6/30 approved changesets -- score normalized to 2",
"points": 3,
"status": "partial",
"details": [],
"max_points": 15
}
]
},
{
"key": "stewardship",
"band": "moderate",
"name": "Ownership & stewardship",
"note": null,
"notes": [],
"value": 51,
"inputs": {
"followers": 5,
"owner_type": "Organization",
"is_verified": null,
"owner_login": "prove-rs",
"public_repos": 2,
"account_age_days": 3017
},
"components": [
{
"key": "ownership_backing",
"name": "Ownership backing",
"detail": "organization-owned",
"points": 30,
"status": "met",
"details": [
{
"code": "owner_organization",
"params": {}
}
],
"max_points": 30
},
{
"key": "verified_domain",
"name": "Verified domain",
"detail": null,
"points": 0,
"status": "missed",
"details": [],
"max_points": 20
},
{
"key": "owner_reach",
"name": "Owner reach",
"detail": "5 followers of prove-rs",
"points": 5.6,
"status": "partial",
"details": [
{
"code": "owner_followers",
"params": {
"count": 5,
"login": "prove-rs"
}
}
],
"max_points": 25
},
{
"key": "track_record",
"name": "Track record",
"detail": "2 public repos, account ~8 yr old",
"points": 15.5,
"status": "partial",
"details": [
{
"code": "public_repos",
"params": {
"count": 2
}
},
{
"code": "account_age_years",
"params": {
"years": 8
}
}
],
"max_points": 25
}
]
},
{
"key": "package_maintenance",
"band": "excellent",
"name": "Package maintenance",
"note": null,
"notes": [],
"value": 100,
"inputs": {
"packages": [
"z3",
"z3-src",
"z3-sys"
],
"ecosystems": "crates",
"any_deprecated": false,
"min_days_since_publish": 0
},
"components": [
{
"key": "published_resolvable",
"name": "Published & resolvable",
"detail": "3 package(s) on crates",
"points": 25,
"status": "met",
"details": [
{
"code": "packages_published",
"params": {
"count": 3,
"ecosystems": "crates"
}
}
],
"max_points": 25
},
{
"key": "publish_recency",
"name": "Publish recency",
"detail": "latest publish 0 days ago",
"points": 35,
"status": "met",
"details": [
{
"code": "publish_recency",
"params": {
"days": 0
}
}
],
"max_points": 35
},
{
"key": "version_history",
"name": "Version history",
"detail": "55 published versions",
"points": 20,
"status": "met",
"details": [
{
"code": "published_versions",
"params": {
"count": 55
}
}
],
"max_points": 20
},
{
"key": "not_deprecated",
"name": "Not deprecated",
"detail": "active, not deprecated or yanked",
"points": 20,
"status": "met",
"details": [
{
"code": "package_not_deprecated",
"params": {}
}
],
"max_points": 20
}
]
}
],
"description": "Will the project survive its people — bus factor, responsiveness, who backs it, and package upkeep?"
},
{
"key": "engineering",
"band": "moderate",
"name": "Engineering Quality",
"value": 64,
"weight": 0.2,
"metrics": [
{
"key": "engineering_practices",
"band": "moderate",
"name": "Engineering practices",
"note": null,
"notes": [],
"value": 66,
"inputs": {
"has_ci": true,
"has_tests": true,
"has_editorconfig": false,
"has_linter_config": false,
"has_precommit_config": false
},
"components": [
{
"key": "ci_workflows",
"name": "CI workflows",
"detail": "3 workflow(s)",
"points": 24,
"status": "met",
"details": [
{
"code": "ci_workflows",
"params": {
"count": 3
}
}
],
"max_points": 24
},
{
"key": "tests_present",
"name": "Tests present",
"detail": null,
"points": 24,
"status": "met",
"details": [],
"max_points": 24
},
{
"key": "linter_config",
"name": "Linter config",
"detail": null,
"points": 0,
"status": "missed",
"details": [],
"max_points": 16
},
{
"key": "pre_commit_hooks",
"name": "Pre-commit hooks",
"detail": null,
"points": 0,
"status": "missed",
"details": [],
"max_points": 9.6
},
{
"key": "editorconfig",
"name": ".editorconfig",
"detail": null,
"points": 0,
"status": "missed",
"details": [],
"max_points": 6.4
},
{
"key": "openssf_scorecard_ci_tests",
"name": "OpenSSF Scorecard: CI-Tests",
"detail": "25 out of 27 merged PRs checked by a CI test -- score normalized to 9",
"points": 18,
"status": "partial",
"details": [],
"max_points": 20
}
]
},
{
"key": "documentation",
"band": "moderate",
"name": "Documentation",
"note": null,
"notes": [],
"value": 60,
"inputs": {
"topics": [
"logic-programming",
"smt",
"smt-solver",
"rust-bindings",
"rust",
"ffi-bindings"
],
"has_wiki": true,
"homepage": null,
"has_readme": true,
"has_docs_dir": false,
"has_description": true
},
"components": [
{
"key": "readme",
"name": "README",
"detail": null,
"points": 30,
"status": "met",
"details": [],
"max_points": 30
},
{
"key": "documentation_directory",
"name": "Documentation directory",
"detail": null,
"points": 0,
"status": "missed",
"details": [],
"max_points": 25
},
{
"key": "documentation_homepage_site",
"name": "Documentation / homepage site",
"detail": null,
"points": 0,
"status": "missed",
"details": [],
"max_points": 15
},
{
"key": "repository_description",
"name": "Repository description",
"detail": null,
"points": 10,
"status": "met",
"details": [],
"max_points": 10
},
{
"key": "topics",
"name": "Topics",
"detail": "6 topics",
"points": 10,
"status": "met",
"details": [
{
"code": "topics_count",
"params": {
"count": 6
}
}
],
"max_points": 10
},
{
"key": "wiki",
"name": "Wiki",
"detail": null,
"points": 10,
"status": "met",
"details": [],
"max_points": 10
}
]
}
],
"description": "Are baseline engineering and documentation practices in place?"
},
{
"key": "security",
"band": "moderate",
"name": "Security",
"value": 54,
"weight": 0.16,
"metrics": [
{
"key": "security_posture",
"band": "at_risk",
"name": "Security posture",
"note": "Excluded from scoring (no data or not applicable): Packaging, Signed-Releases. Remaining weights renormalized.",
"notes": [
{
"code": "excluded_no_data",
"params": {
"components": [
"packaging",
"signed_releases"
]
}
},
{
"code": "weights_renormalized",
"params": {}
}
],
"value": 42,
"inputs": {
"source": "openssf_scorecard",
"checks_evaluated": 16,
"scorecard_version": "v5.5.0",
"checks_inconclusive": 2,
"scorecard_aggregate": 4.2
},
"components": [
{
"key": "binary_artifacts",
"name": "Binary-Artifacts",
"detail": "no binaries found in the repo",
"points": 7.5,
"status": "met",
"details": [],
"max_points": 7.5
},
{
"key": "branch_protection",
"name": "Branch-Protection",
"detail": "branch protection not enabled on development/release branches",
"points": 0,
"status": "missed",
"details": [],
"max_points": 7.5
},
{
"key": "ci_tests",
"name": "CI-Tests",
"detail": "25 out of 27 merged PRs checked by a CI test -- score normalized to 9",
"points": 2.2,
"status": "partial",
"details": [],
"max_points": 2.5
},
{
"key": "cii_best_practices",
"name": "CII-Best-Practices",
"detail": "no effort to earn an OpenSSF best practices badge detected",
"points": 0,
"status": "missed",
"details": [],
"max_points": 2.5
},
{
"key": "code_review",
"name": "Code-Review",
"detail": "Found 6/30 approved changesets -- score normalized to 2",
"points": 1.5,
"status": "partial",
"details": [],
"max_points": 7.5
},
{
"key": "contributors",
"name": "Contributors",
"detail": "project has 26 contributing companies or organizations",
"points": 2.5,
"status": "met",
"details": [],
"max_points": 2.5
},
{
"key": "dangerous_workflow",
"name": "Dangerous-Workflow",
"detail": "no dangerous workflow patterns detected",
"points": 10,
"status": "met",
"details": [],
"max_points": 10
},
{
"key": "dependency_update_tool",
"name": "Dependency-Update-Tool",
"detail": "no update tool detected",
"points": 0,
"status": "missed",
"details": [],
"max_points": 7.5
},
{
"key": "fuzzing",
"name": "Fuzzing",
"detail": "project is not fuzzed",
"points": 0,
"status": "missed",
"details": [],
"max_points": 5
},
{
"key": "license",
"name": "License",
"detail": "license file not detected",
"points": 0,
"status": "missed",
"details": [],
"max_points": 2.5
},
{
"key": "maintained",
"name": "Maintained",
"detail": "10 commit(s) and 4 issue activity found in the last 90 days -- score normalized to 10",
"points": 7.5,
"status": "met",
"details": [],
"max_points": 7.5
},
{
"key": "packaging",
"name": "Packaging",
"detail": "packaging workflow not detected",
"points": 0,
"status": "excluded",
"details": [
{
"code": "no_data",
"params": {}
}
],
"max_points": 5
},
{
"key": "pinned_dependencies",
"name": "Pinned-Dependencies",
"detail": "dependency not pinned by hash detected -- score normalized to 0",
"points": 0,
"status": "missed",
"details": [],
"max_points": 5
},
{
"key": "sast",
"name": "SAST",
"detail": "SAST tool is not run on all commits -- score normalized to 0",
"points": 0,
"status": "missed",
"details": [],
"max_points": 5
},
{
"key": "security_policy",
"name": "Security-Policy",
"detail": "security policy file not detected",
"points": 0,
"status": "missed",
"details": [],
"max_points": 5
},
{
"key": "signed_releases",
"name": "Signed-Releases",
"detail": "no releases found",
"points": 0,
"status": "excluded",
"details": [
{
"code": "no_data",
"params": {}
}
],
"max_points": 7.5
},
{
"key": "token_permissions",
"name": "Token-Permissions",
"detail": "detected GitHub workflow tokens with excessive permissions",
"points": 0,
"status": "missed",
"details": [],
"max_points": 7.5
},
{
"key": "vulnerabilities",
"name": "Vulnerabilities",
"detail": "0 existing vulnerabilities detected",
"points": 7.5,
"status": "met",
"details": [],
"max_points": 7.5
}
]
},
{
"key": "dependency_advisories",
"band": "excellent",
"name": "Dependency advisories",
"note": "Excluded from scoring (no data or not applicable): No advisories left outstanding. Remaining weights renormalized. Matched the crates:z3@0.20.2 runtime dependency closure — what installing the published package pulls in — 20 packages. Reachability is not analyzed.",
"notes": [
{
"code": "excluded_no_data",
"params": {
"components": [
"no_advisories_left_outstanding"
]
}
},
{
"code": "weights_renormalized",
"params": {}
},
{
"code": "advisories_scope_published",
"params": {
"package": "crates:z3@0.20.2",
"assessed": 20
}
},
{
"code": "advisories_reachability",
"params": {}
}
],
"value": 100,
"inputs": {
"source": "osv",
"advisories": 0,
"affected_packages": 0,
"assessed_packages": 20,
"unassessed_packages": 0,
"affected_by_severity": "none",
"direct_affected_packages": 0
},
"components": [
{
"key": "direct_dependencies_free_of_known_advisories",
"name": "Direct dependencies free of known advisories",
"detail": "no direct dependency carries a known advisory",
"points": 35,
"status": "met",
"details": [
{
"code": "no_direct_advisories",
"params": {}
}
],
"max_points": 35
},
{
"key": "indirect_dependencies_free_of_known_advisories",
"name": "Indirect dependencies free of known advisories",
"detail": "no indirect dependency carries a known advisory",
"points": 25,
"status": "met",
"details": [
{
"code": "no_indirect_advisories",
"params": {}
}
],
"max_points": 25
},
{
"key": "no_advisories_left_outstanding",
"name": "No advisories left outstanding",
"detail": "no advisory carries a publication date",
"points": 0,
"status": "excluded",
"details": [
{
"code": "advisories_no_publication_date",
"params": {}
}
],
"max_points": 40
}
]
},
{
"key": "malicious_dependencies",
"band": "excellent",
"name": "Malicious dependencies",
"note": null,
"notes": [],
"value": 100,
"inputs": {
"source": "osv",
"meaning": "reported as a malicious package by the OpenSSF corpus; the remedy is removal or moving off the compromised name, never an upgrade of the same artifact. Versions the registry has since pulled are listed but not scored",
"packages": [],
"red_flag": false,
"assessed_packages": 20,
"malicious_packages": 0,
"direct_malicious_packages": 0,
"withdrawn_malicious_packages": 0,
"installable_malicious_packages": 0
},
"components": [
{
"key": "no_dependency_reported_as_a_malicious_package",
"name": "No dependency reported as a malicious package",
"detail": "no dependency is reported as a malicious package",
"points": 100,
"status": "met",
"details": [
{
"code": "no_malicious_dependencies",
"params": {}
}
],
"max_points": 100
}
]
},
{
"key": "high_risk_jurisdiction_exposure",
"band": "excellent",
"name": "High-Risk Jurisdiction Exposure",
"note": "Only high-confidence self-published location evidence affects this multiplier. Ambiguous matches are review-only; country evidence is not proof of nationality, citizenship, legal registration, malicious intent, or sanctions status.",
"notes": [
{
"code": "jurisdiction_evidence_limits",
"params": {}
}
],
"value": 100,
"inputs": {
"meaning": "self-published location evidence; not nationality or citizenship",
"red_flag": false,
"exposures": [],
"policy_countries": [
"Russia",
"Iran",
"North Korea"
],
"review_only_matches": 0,
"assessed_self_published_locations": 8
},
"components": [
{
"key": "policy_exposure_multiplier",
"name": "Policy exposure multiplier",
"detail": "no confirmed policy-scope location match",
"points": 100,
"status": "met",
"details": [
{
"code": "jurisdiction_no_match",
"params": {}
}
],
"max_points": 100
}
]
}
],
"description": "Are visible security and supply-chain practices strong, with no malicious dependency and no unresolved high-risk jurisdiction exposure?"
},
{
"key": "ai_readiness",
"band": "moderate",
"name": "AI Readiness",
"value": 53,
"weight": 0,
"metrics": [
{
"key": "ai_agent_context",
"band": "at_risk",
"name": "Agent context & guidance",
"note": null,
"notes": [],
"value": 40,
"inputs": {
"has_llms_txt": false,
"legible_history_share": 0.99,
"agent_instruction_files": [],
"agent_instruction_max_bytes": null
},
"components": [
{
"key": "agent_instructions",
"name": "Agent instructions",
"detail": "no CLAUDE.md / AGENTS.md / editor rules",
"points": 0,
"status": "missed",
"details": [
{
"code": "no_agent_instructions",
"params": {}
}
],
"max_points": 45
},
{
"key": "machine_readable_docs_llms_txt",
"name": "Machine-readable docs (llms.txt)",
"detail": null,
"points": 0,
"status": "missed",
"details": [],
"max_points": 15
},
{
"key": "legible_commit_history",
"name": "Legible commit history",
"detail": "99 of 100 human commits state their intent (structured subject or explanatory body)",
"points": 40,
"status": "met",
"details": [
{
"code": "legible_history",
"params": {
"legible": 99,
"sampled": 100
}
}
],
"max_points": 40
}
]
},
{
"key": "ai_verify_loop",
"band": "at_risk",
"name": "Verify loop (build / test / typecheck)",
"note": null,
"notes": [],
"value": 46,
"inputs": {
"has_nix": false,
"has_tests": true,
"lockfiles": [],
"has_dockerfile": false,
"typed_language": true,
"bootstrap_files": [],
"has_devcontainer": false,
"has_linter_config": false,
"typecheck_configs": [],
"agent_commit_share": 0,
"toolchain_manifests": [
"Cargo.toml",
"xtask/Cargo.toml",
"z3-src/Cargo.toml",
"z3-sys/Cargo.toml",
"z3/Cargo.toml"
],
"dependency_bot_commit_share": 0
},
"components": [
{
"key": "one_command_bootstrap",
"name": "One-command bootstrap",
"detail": "Cargo.toml, xtask/Cargo.toml, z3-src/Cargo.toml (toolchain convention, no task runner)",
"points": 12.6,
"status": "partial",
"details": [
{
"code": "toolchain_convention",
"params": {
"files": "Cargo.toml, xtask/Cargo.toml, z3-src/Cargo.toml"
}
}
],
"max_points": 18
},
{
"key": "automated_tests",
"name": "Automated tests",
"detail": null,
"points": 22,
"status": "met",
"details": [],
"max_points": 22
},
{
"key": "lint_format_config",
"name": "Lint / format config",
"detail": null,
"points": 0,
"status": "missed",
"details": [],
"max_points": 11
},
{
"key": "static_type_checking",
"name": "Static type checking",
"detail": "Rust (statically typed)",
"points": 11,
"status": "met",
"details": [
{
"code": "statically_typed_language",
"params": {
"language": "Rust"
}
}
],
"max_points": 11
},
{
"key": "reproducible_environment",
"name": "Reproducible environment",
"detail": null,
"points": 0,
"status": "missed",
"details": [],
"max_points": 10
},
{
"key": "demonstrated_agent_practice",
"name": "Demonstrated agent practice",
"detail": "no agent-authored commits among the last 100",
"points": 0,
"status": "missed",
"details": [
{
"code": "no_agent_authored_commits",
"params": {
"sampled": 100
}
}
],
"max_points": 10
},
{
"key": "automated_maintenance",
"name": "Automated maintenance",
"detail": "no automated dependency updates observed",
"points": 0,
"status": "missed",
"details": [
{
"code": "no_dependency_automation",
"params": {}
}
],
"max_points": 8
},
{
"key": "openssf_scorecard_pinned_dependencies",
"name": "OpenSSF Scorecard: Pinned-Dependencies",
"detail": "dependency not pinned by hash detected -- score normalized to 0",
"points": 0,
"status": "missed",
"details": [],
"max_points": 10
}
]
},
{
"key": "ai_code_legibility",
"band": "excellent",
"name": "Code legibility for models",
"note": null,
"notes": [],
"value": 100,
"inputs": {
"primary_language": "Rust",
"largest_source_bytes": 56019,
"source_files_sampled": 64,
"oversized_source_files": 0
},
"components": [
{
"key": "type_checkable_code",
"name": "Type-checkable code",
"detail": "Rust (statically typed)",
"points": 45,
"status": "met",
"details": [
{
"code": "statically_typed_language",
"params": {
"language": "Rust"
}
}
],
"max_points": 45
},
{
"key": "manageable_file_sizes",
"name": "Manageable file sizes",
"detail": "0/64 source files over 60KB",
"points": 55,
"status": "met",
"details": [
{
"code": "oversized_source_files",
"params": {
"kb": 60,
"sampled": 64,
"oversized": 0
}
}
],
"max_points": 55
}
]
}
],
"description": "How well is the repo equipped to be developed and maintained with AI coding agents? An independent, experimental badge — weight 0.0, so it is surfaced on its own and does not affect the overall health score."
}
],
"metrics_version": "1.13.0"
},
"warnings": [
"Star history unavailable: GitHub GraphQL error: Resource not accessible by personal access token",
"crates package 'xtask' points at a different repository (https://github.com/arcboxlabs/xtask); excluded from ecosystem scoring"
],
"report_type": "repository",
"generated_at": "2026-07-23T15:29:03.477686Z",
"schema_version": "0.27.0",
"badge_url": "https://raw.githubusercontent.com/inspect-software/badges/main/v1/p/prove-rs/z3.rs.svg",
"full_name": "prove-rs/z3.rs",
"license_state": "absent",
"license_spdx": null
}Оцінки — це сигнали, а не гарантії. Вони відображають публічно видимі практики на GitHub — це не аудит коду й не гарантія безпеки.
Відсутні дані виключаються, а ваги перенормовуються — нуль за відсутність ніколи не ставиться. Методологія версіонована й відкрита: метрики v1.13.0, схема v0.27.0 — повна методологія · вікі метрик.
Як окремий результат виглядає на тлі всього реєстру: сукупна статистика — crates.io.