Registro públicoModerado
Informe de salud del softwareesquema 0.27.0 · métricas 1.13.0 · 2026-07-23 15:29 UTC
prove-rs / z3.rs
Rust bindings for the Z3 solver.
prove-rs/z3.rs tiene un índice de salud de 69 sobre 100, lo que lo sitúa en la banda Moderado. Su puntuación más alta es Vitality (89/100) y la más baja, AI Readiness (53/100). Se actualizó por última vez hoy. 3 personas concentran la mayor parte del trabajo reciente.
69
global / 100Índice de salud del software
Las métricas se agrupan en categorías ponderadas sobre una escala de 1 a 100. El resultado global parte de su media; cuando la evidencia pública activa la Política de Jurisdicciones de Alto Riesgo, la calificación se ajusta y recibe el límite 49 (En riesgo). Preparación para IA queda fuera.
69
Excelente85-100Ejemplar; cumple prácticamente todos los criterios evaluados
Bueno70-84Saludable; carencias menores
Moderado50-69Aceptable con carencias notables; se recomienda revisión
En riesgo30-49Debilidades significativas; su adopción exige cautela
Crítico1-29Problemas graves (proyecto abandonado, un solo mantenedor, sin higiene)
Perfil de puntuación
Cada eje es una categoría. La forma importa más que la media: un proyecto sano llena toda la figura, mientras que un perfil de picos y cráteres indica que la fortaleza en una dimensión enmascara el riesgo en otra.
Titularidad
prove-rsOrganización
5 seguidores2 repositorios públicosdesde abr 2018
Este repositorio está respaldado por una organización: una custodia compartida y responsable que puede sobrevivir a cualquier mantenedor individual.
Ecosistemas de paquetes
| Registro | Paquete | Versión | Descargas / mes | Versiones | Última publicación | Etiquetas |
|---|---|---|---|---|---|---|
| crates.io | z3 | 0.20.2 | 164.435 | 55 | hace 26 días | ffisolversmtsatisfiabilityapi-bindings |
| crates.io | xtaskapunta a otro repositorio; no se puntúa | 0.1.4 | 185 | 5 | hace 23 días | automationmacosreleasecodesignxtaskcommand-line-utilities |
| crates.io | z3-src | 500.0.0 | 9492 | 10 | hace 0 días | solverbuildsmtsatisfiability |
| crates.io | z3-sys | 0.12.0 | 165.755 | 36 | hace 0 días | ffisolversmtsatisfiabilityno-stdexternal-ffi-bindings |
Métricas por categoría
Vitalidad
¿Está vivo el proyecto: se escribe código y se publican versiones?
89
Actividad de desarrollo
81Bueno
Cómo se puntúa
| 36/36 | Recencia de push — último push hace 0 días |
| 17.3/36 | Cadencia de commits — 25/52 semanas con commits |
| 18/18 | Volumen de commits — 114 commits en el último año |
| 10/10 | OpenSSF Scorecard: Maintained — 10 commit(s) and 4 issue activity found in the last 90 days -- score normalized to 10 |
Datos de entrada utilizados
| commits_last_year | 114 |
| human_commit_share | 1 |
| days_since_last_push | 0 |
| active_weeks_last_year | 25 |
Disciplina de publicación
100Excelente
Cómo se puntúa
| 27/27 | Publica versiones — 61 versiones publicadas |
| 36/36 | Recencia de las versiones — última versión hace 0 días |
| 27/27 | Cadencia de publicación — una versión cada ~14,7 días |
| 0/10 | OpenSSF Scorecard: Signed-Releases — sin datos |
Datos de entrada utilizados
| releases_count | 61 |
| latest_release_tag | z3-sys-v0.12.0 |
| releases_from_tags | no |
| days_since_latest_release | 0 |
| mean_days_between_releases | 14,7 |
Excluidos de la puntuación (sin datos o no aplicable): OpenSSF Scorecard: Signed-Releases. Los pesos restantes se han renormalizado.
Comunidad y Adopción
¿Tiene el proyecto usuarios, descargas, atención y unas condiciones acogedoras para quienes contribuyen?
58
Popularidad y adopción
66Moderado
Cómo se puntúa
| 44.1/60 | Estrellas — 522 estrellas |
| 18.2/25 | Forks — 153 forks |
| 3.9/15 | Observadores — 6 observadores |
Datos de entrada utilizados
| forks | 153 |
| stars | 522 |
| watchers | 6 |
| growth_state | unverified |
| growth_factor_pct | 100 |
| growth_unverified_reason | no_history |
Salud de la comunidad
25Crítico
Cómo se puntúa
| 22.5/22.5 | README |
| 0/22.5 | Licencia — no se detectó ningún archivo de licencia |
| 0/18 | Guía CONTRIBUTING |
| 0/13.5 | Código de conducta |
| 0/7.2 | Plantilla de issues |
| 0/6.3 | Plantilla de PR |
Datos de entrada utilizados
| has_readme | sí |
| has_license | no |
| has_contributing | no |
| has_issue_template | no |
| has_code_of_conduct | no |
| has_pull_request_template | no |
Adopción en el ecosistema (descargas)
92Excelente
Cómo se puntúa
| 73.7/80 | Descargas mensuales — 339.682 descargas/mes en crates |
| 0/20 | Dependientes en el registro — no lo informa este ecosistema |
Datos de entrada utilizados
| packages | z3, z3-src, z3-sys |
| dependents | — |
| ecosystems | crates |
| total_downloads | 3.061.744 |
| monthly_downloads | 339.682 |
Excluidos de la puntuación (sin datos o no aplicable): Dependientes en el registro. Los pesos restantes se han renormalizado.
Sostenibilidad y Gobernanza
¿Sobrevivirá el proyecto a sus personas: factor bus, capacidad de respuesta, quién lo respalda y mantenimiento del paquete?
74
Cómo se puntúa
| 36/54 | Factor bus — la mitad de los commits recae en 3 contribuyente(s) |
| 15.5/22.5 | Distribución de commits — el principal contribuyente firma el 31% de los commits |
| 13.5/13.5 | Amplitud de contribuyentes — 78 contribuyentes |
| 10/10 | OpenSSF Scorecard: Contributors — project has 26 contributing companies or organizations |
Datos de entrada utilizados
| bus_factor | 3 |
| contributors_sampled | 78 |
| top_contributor_share | 0,309 |
Cómo se puntúa
| 37.3/46.8 | Resolución de issues — 80% de issues cerradas |
| 34.2/38.3 | Aceptación de PR — 328/367 PR decididos fusionados |
| 3/15 | OpenSSF Scorecard: Code-Review — Found 6/30 approved changesets -- score normalized to 2 |
Datos de entrada utilizados
| merged_prs | 328 |
| open_issues | 37 |
| closed_issues | 145 |
| issue_closed_ratio | 0,797 |
| closed_unmerged_prs | 39 |
Propiedad y custodia
51Moderado
Cómo se puntúa
| 30/30 | Respaldo de la propiedad — propiedad de una organización |
| 0/20 | Dominio verificado |
| 5.6/25 | Alcance del propietario — 5 seguidores de prove-rs |
| 15.5/25 | Trayectoria — 2 repos públicos, cuenta de ~8 años |
Datos de entrada utilizados
| followers | 5 |
| owner_type | Organization |
| is_verified | — |
| owner_login | prove-rs |
| public_repos | 2 |
| account_age_days | 3017 |
Mantenimiento de paquetes
100Excelente
Cómo se puntúa
| 25/25 | Publicado y resoluble — 3 paquete(s) en crates |
| 35/35 | Recencia de publicación — última publicación hace 0 días |
| 20/20 | Historial de versiones — 55 versiones en el registro |
| 20/20 | No obsoleto — activo, ni obsoleto ni retirado |
Datos de entrada utilizados
| packages | z3, z3-src, z3-sys |
| ecosystems | crates |
| any_deprecated | no |
| min_days_since_publish | 0 |
Calidad de Ingeniería
¿Existen unas prácticas mínimas de ingeniería y documentación?
64
Prácticas de ingeniería
66Moderado
Cómo se puntúa
| 24/24 | Flujos de trabajo de CI — 3 flujo(s) de trabajo |
| 24/24 | Pruebas presentes |
| 0/16 | Configuración de linter |
| 0/9.6 | Hooks de 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 |
Datos de entrada utilizados
| has_ci | sí |
| has_tests | sí |
| has_editorconfig | no |
| has_linter_config | no |
| has_precommit_config | no |
Documentación
60Moderado
Cómo se puntúa
| 30/30 | README |
| 0/25 | Directorio de documentación |
| 0/15 | Sitio de documentación / página del proyecto |
| 10/10 | Descripción del repositorio |
| 10/10 | Topics — 6 topics |
| 10/10 | Wiki |
Datos de entrada utilizados
| topics | logic-programming, smt, smt-solver, rust-bindings, rust, ffi-bindings |
| has_wiki | sí |
| homepage | — |
| has_readme | sí |
| has_docs_dir | no |
| has_description | sí |
Seguridad
¿Son sólidas las prácticas visibles de seguridad y de cadena de suministro, sin exposición jurisdiccional de alto riesgo sin resolver?
54
Postura de seguridad
42En riesgo
Cómo se puntúa
| 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 | Licencia — 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 — sin datos |
| 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 — sin datos |
| 0/7.5 | Token-Permissions — detected GitHub workflow tokens with excessive permissions |
| 7.5/7.5 | Vulnerabilities — 0 existing vulnerabilities detected |
Datos de entrada utilizados
| source | openssf_scorecard |
| checks_evaluated | 16 |
| scorecard_version | v5.5.0 |
| checks_inconclusive | 2 |
| scorecard_aggregate | 4,2 |
Excluidos de la puntuación (sin datos o no aplicable): packaging, signed_releases. Los pesos restantes se han renormalizado.
Avisos de dependencias
100Excelente
Cómo se puntúa
| 35/35 | Dependencias directas libres de avisos conocidos — ninguna dependencia directa tiene un aviso conocido |
| 25/25 | Dependencias indirectas libres de avisos conocidos — ninguna dependencia indirecta tiene un aviso conocido |
| 0/40 | Sin avisos pendientes — ningún aviso tiene fecha de publicación |
Datos de entrada utilizados
| source | osv |
| advisories | 0 |
| affected_packages | 0 |
| assessed_packages | 20 |
| unassessed_packages | 0 |
| affected_by_severity | none |
| direct_affected_packages | 0 |
Excluidos de la puntuación (sin datos o no aplicable): Sin avisos pendientes. Los pesos restantes se han renormalizado. Se cotejó el cierre de dependencias en tiempo de ejecución de crates:z3@0.20.2 —lo que arrastra la instalación del paquete publicado—: 20 paquetes. No se analiza la alcanzabilidad.
Preparación para IA
¿Hasta qué punto está el repositorio preparado para desarrollarse y mantenerse con agentes de codificación de IA? Es una insignia independiente y experimental — peso 0,0, de modo que se presenta por separado y no afecta a la puntuación de salud global.
53
Contexto y guía para agentes
40En riesgo
Cómo se puntúa
| 0/45 | Instrucciones para agentes — sin CLAUDE.md / AGENTS.md / reglas de editor |
| 0/15 | Documentación legible por máquinas (llms.txt) |
| 40/40 | Historial de commits legible — 99 de 100 commits humanos declaran su intención (asunto estructurado o cuerpo explicativo) |
Datos de entrada utilizados
| has_llms_txt | no |
| legible_history_share | 0,99 |
| agent_instruction_files | — |
| agent_instruction_max_bytes | — |
Cómo se puntúa
| 12.6/18 | Arranque con un solo comando — Cargo.toml, xtask/Cargo.toml, z3-src/Cargo.toml (convención del toolchain, sin ejecutor de tareas) |
| 22/22 | Pruebas automatizadas |
| 0/11 | Configuración de lint / formato |
| 11/11 | Verificación estática de tipos — Rust (tipado estático) |
| 0/10 | Entorno reproducible |
| 0/10 | Práctica demostrada con agentes — ningún commit con autoría de agente entre los últimos 100 |
| 0/8 | Mantenimiento automatizado — no se observan actualizaciones automáticas de dependencias |
| 0/10 | OpenSSF Scorecard: Pinned-Dependencies — dependency not pinned by hash detected -- score normalized to 0 |
Datos de entrada utilizados
| has_nix | no |
| has_tests | sí |
| lockfiles | — |
| has_dockerfile | no |
| typed_language | sí |
| bootstrap_files | — |
| has_devcontainer | no |
| has_linter_config | no |
| 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 |
Legibilidad del código para modelos
100Excelente
Cómo se puntúa
| 45/45 | Código verificable por tipos — Rust (tipado estático) |
| 55/55 | Tamaños de archivo manejables — 0/64 archivos fuente de más de 60 KB |
Datos de entrada utilizados
| primary_language | Rust |
| largest_source_bytes | 56.019 |
| source_files_sampled | 64 |
| oversized_source_files | 0 |
Datos clave
522estrellas de GitHub
78contribuidores
114commits en los últimos 12 meses
0días desde el último push
61versiones publicadas
3factor bus
37issues abiertas
crates.ioecosistemas de paquetes
Advertencias de recopilación de datos
- 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
Más detalle
Historial de estrellas y forks 0 ★ / 153 ⇿
0Estrellas
153Forks
58Versiones
Cuándo se añadió cada estrella y fork, recopilado de GitHub y agrupado por día. El crecimiento acumulado se sitúa justo encima de las adiciones diarias que lo componen, de modo que ambos se leen en conjunto: la acumulación orgánica sostenida no se parece en nada a un pico abrupto y efímero. Cuando esa diferencia es medible, se informa como autenticidad del crecimiento.
Mayor 0Menor 0Parche 0
Cada punto abarca 8 días.
OpenSSF Scorecard 4.2 / 10
4.2agregado
Evaluación de seguridad independiente y agnóstica en cuanto a herramientas, procedente del proyecto de código abierto OpenSSF Scorecard. Cada comprobación premia una práctica de seguridad, no la herramienta de un proveedor concreto. Las comprobaciones que Scorecard no pudo determinar se marcan como n/d y se excluyen de la puntuación de seguridad (nunca se cuentan como cero).
| 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 |
| n/d | 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 |
| n/d | Signed-Releases | no releases found |
| 0 | Token-Permissions | detected GitHub workflow tokens with excessive permissions |
| 10 | Vulnerabilities | 0 existing vulnerabilities detected |
Dependencias directas 6
| Registro | Paquete | Restricción de versión | Manifiesto |
|---|---|---|---|
| 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 |
Todas las dependencias 20
Conjunto completo de dependencias resueltas según el grafo de dependencias de GitHub: 6 paquetes directos y 14 indirectos (transitivos). El cierre transitivo es completo cuando el repositorio incluye un lockfile.
| Registro | Paquete | Versión | Relación |
|---|---|---|---|
| crates.io | clap | — | directa |
| crates.io | cmake | — | directa |
| crates.io | log | — | directa |
| crates.io | num | — | directa |
| crates.io | semver | — | directa |
| crates.io | z3-sys | — | directa |
| crates.io | bindgen | — | indirecta |
| crates.io | env_logger | — | indirecta |
| crates.io | pkg-config | — | indirecta |
| crates.io | prettyplease | — | indirecta |
| crates.io | proc-macro2 | — | indirecta |
| crates.io | quote | — | indirecta |
| crates.io | rayon | — | indirecta |
| crates.io | regex | — | indirecta |
| crates.io | reqwest | — | indirecta |
| crates.io | serde_json | — | indirecta |
| crates.io | syn | — | indirecta |
| crates.io | vcpkg | — | indirecta |
| crates.io | z3-src | — | indirecta |
| crates.io | zip | — | indirecta |
Avisos de dependencias 0
Instalar crates:z3@0.20.2 arrastra 20 paquetes, directos y transitivos: 0 tienen avisos conocidos, de los cuales 0 son dependencias directas.
Ningún aviso conocido afecta a las dependencias evaluadas.
Un aviso significa que la versión registrada en el grafo de dependencias cae dentro del rango afectado de un aviso. No se analiza la alcanzabilidad, y el grafo incluye fijaciones de desarrollo y prueba: un hallazgo puede referirse al utillaje y no al software distribuido.
Informe JSON sin procesar legible por máquina
{
"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
}Las puntuaciones son señales, no garantías. Reflejan prácticas públicamente visibles en GitHub; no son una auditoría de código ni una garantía de seguridad.
Los datos ausentes se excluyen y los pesos se renormalizan; nunca se puntúan como cero. La metodología es versionada y abierta: métricas v1.13.0, esquema v0.27.0 — metodología completa · wiki de métricas.
Cómo se sitúa un resultado dentro del registro general: estadísticas agregadas — crates.io.