provable

Exact audit, surgery, and certified discovery for tree ensembles.

provable treats a fitted model as an auditable artifact. On xgboost models it reads an exact itemization of every rule the model uses (the transported atom spectrum), checks it against a declared policy, removes forbidden rule families by appended-tree surgery whose output is still a valid native model file, and emits a tamper-evident certificate dossier that a third party can re-check with an independent, numpy-only verifier that shares no code with the engine. On raw data it runs the certified-discovery sieve: an FDR-controlled claims ledger, a dark-mass ledger, and the right to refuse (k = 0 is a verdict, not an error).

• Tests that ship with the code: 35 pytest tests, the 17-item acceptance ledger (tests/selftest.py, T1-T7), and a verifier mutation battery.
• Independent verification: every certificate is re-checked by provable-verify - numpy + stdlib only, zero shared code with the engine, machine-enforced in CI.
• Reproducibility: the archived DOI version of this package (10.5281/zenodo.21819947) reproduces every number in the papers.
• Version 0.9.0. It becomes 1.0.0 when the evidence-bundle schema and the enforce API freeze.

            ┌─ WORKFLOW A: audit a model ────────────────────────────────────────┐
model.json ─► load ────► transported atom spectrum (exact, leaf-readable)        │
Policy ─────► audit ───► verdict + findings: masses, shares, threshold locations │
            │ enforce ─► appended-tree surgery ─► model_v2.json (still native)   │
            │            + dossier: evidence.json · certificate.md · MANIFEST   │
            │ verify ──► independent re-check (own parser, own predictor,        │
            │            own transport; zero shared code; numpy + stdlib only)   │
            └────────────────────────────────────────────────────────────────────┘
            ┌─ WORKFLOW B: interrogate data ─────────────────────────────────────┐
X, y ───────► discover (certified sieve) ─► FDR claims ledger · two-tier         │
            │ predictor · toll/penumbra diagnostics · dark-mass ledger ·         │
            │ phase verdict (I / II-a / II-b / III) · or refusal at k = 0        │
            └────────────────────────────────────────────────────────────────────┘

The two workflows share one substrate — the atom schema (threshold predicates and their conjunctions) — so a violation found in a model (A) can be interrogated in the data (B): is this pattern a property of your model, or of your world?

One repo, two distributions

The verifier re-implements from the xgboost JSON spec its own parser, its own vectorized tree-walk predictor, and its own transport expansion. Independence is machine-checked: tests/test_firewall.py fails CI on any verifier import outside {stdlib, numpy} or any import of the engine.

The checker also ships standalone at github.com/provable-ml/provable-verify, a byte-identical mirror of verify/; changes land in this repository first and are mirrored there.

Install

From PyPI:

pip install provable
pip install provable-verify

Working from a clone (editable installs of both distributions):

pip install -e .            # provable (engine): pulls numpy, pandas, scipy, scikit-learn,
pip install -e ./verify     # provable-verify (checker): numpy only     statsmodels, xgboost, tabulate, plotly, qrcode

After this, import provable works anywhere in the venv and the verifier runs as python -m provable_verify <evidence.json> <model.json> from any directory (file arguments are relative to your cwd -- the demo dossier lives in dossier_demo/).

Tested with Python 3.12, xgboost 3.3.0 (adapter write-back exercised on 3.3.0 only so far; needs xgboost ≥ 2.0). The verifier needs numpy only.

Quickstart A — audit, enforce, verify

import xgboost as xgb
from provable import audit, enforce, Policy, between

policy = Policy([between('age', 'group_A')], name='fair_lending_demo')

# Audit an EXTERNAL artifact you did not train
a = audit('model.json', policy, X_val, out_dir='dossier_audit')
a['verdict']['state']            # 'PASS' | 'FINDINGS' | 'DECLINED'
a['findings']                    # per clause: n_atoms, exact data mass, share of
                                 # model variance, threshold locations

# Remove the family; output is a still-valid native model
b = enforce('model.json', policy, X_train, X_holdout, 'model_v2.json',
            y_holdout=y_holdout, out_dir='dossier_enforce')

m2 = xgb.Booster(); m2.load_model('model_v2.json')   # loads in STOCK xgboost

$ python -m provable_verify dossier_enforce/evidence.json model_v2.json
  [PASS] 1 bundle hash = certificate id
  [PASS] 2 model file hash matches bundle
  [PASS] 3 policy hash matches bundle
  [PASS] 4 structural probe (own transport)
  [PASS] 5 behavioral probe (own predictor)
  [PASS] 6 verdict supported by own probes
  [PASS] 7 limits panel present
VERIFICATION: PASS

Data contract (A). X is numeric (ndarray or DataFrame values); feature names come from the model artifact. Predicates are evaluated in float32 with xgboost's own routing semantics (x < c → left), so threshold-boundary rows route identically in the spectrum and the stock engine. NaN anywhere in X is a coded refusal (R-07): audit returns DECLINED, enforce raises — the transported audit is not defined for missing-value routing, and the tool says so rather than guessing.

Quickstart B — certified discovery

from provable import CertifiedDiscovery

cd = CertifiedDiscovery(stability_reps=8, seed=0)
report = cd.run(X_df, y)                    # X_df: DataFrame (mixed dtypes), y: 1-D numeric
cd.plot()                                   # 4-panel plotly figure
cd.claims_                                  # certified claims ledger (DataFrame)
p = cd.predict(X_new, model='two_tier')     # 'two_tier' | 'certified' | 'xgb'

Data contract (B). Numeric columns get threshold atoms, non-numeric columns get one-hot atoms; NaN makes every predicate evaluate to False (the engine receives NaN natively). If y ⊆ {0, 1} the run is a linear probability model: MSE/Brier primary, AUC also reported; predictions are not clipped to [0, 1].

The dossier

Every audit/enforce run with out_dir emits:

dossier/
├── evidence.json     canonical bundle -- the source of truth; certificate id =
│                     'PV-' + sha256(canonical bundle)[:16]
├── certificate.md   human rendering (GitHub-renderable markdown) bound to the same bundle
└── (enforce)         model_v2.json, MANIFEST.sha256, HOW_TO_VERIFY.txt in the demo

Marks used everywhere: #exact — an arithmetic fact of the artifact (structural zeros, masses, prices; no error bar exists). #est — a statistical estimate, always with its interval. The limits panel ("what this does not establish": proxies, causal claims, off-distribution behavior, NaN routing) is furniture, not fine print: every bundle carries it and verifier check 7 fails if it is stripped.

Verdict grammar

What "exact" means here (workflow A)

A fitted ensemble on continuous inputs is already a Boolean object on its own split thresholds. Each leaf box expands exactly:

1[lo <= x < hi] = 1[x >= lo] - 1[x >= hi]        (per feature; telescoped over the box)

so the whole artifact equals base_score + Σ coef · AND_f 1[x_f >= t_f] — a finite, leaf-readable, signed rule spectrum with no sampling and no approximation. Audit families, prices, surgery, and both certification probes operate on this identity.

Measured on the shipped acceptance ledger (tests/selftest.py, 17/17, xgboost 3.3.0, 200-tree depth-4 external artifact, 4,676 atoms):

The sieve (workflow B)

raw X, y
  ├─ engine:      XGBoost on raw features (early-stopped on a carve of the training rows)
  └─ instrument:  atom dictionary ─► RS(ν,R) proposal on S1 ─► forward core ─► one OLS
                  pass on S2 + BH(q) ─► certified model ─► claim-free halo ─► two-tier
diagnostics:      penumbra · toll bounds · spotlight margin · completion · phase · ledger
report:           console tables + plotly figure + machine-readable dict + claims DataFrame

The gate is one selection-conditional OLS pass on the reserved half S2 with BH(q) over partial-t p-values; every quoted effect, CI, t, p comes from that single pass. The halo is claim-free (using the two-tier predictor never touches the ledger's guarantee). The dark-mass ledger splits Var(y) into legible (certified), dark-to-certification-but- visible-to-engine, and engine MSE (noise + dark to both). Phases: I (refusal competitive or k = 0), II-a (engine ahead, frame-blind margin M_C > 0), II-b (engine ahead, M_C ≤ 0), III-like (certified core ahead on test).

Key parameters (defaults): fdr_q=0.10, rounds=4, entry_t=2.0, entry_cap=300, core_cap=120, core_tmin=1.0, n_cuts=8, cart_cuts=True, n_harvest=40, interactions=True (shadow rule conj_shadow=0.9), prune_support=0.005, prune_dup_r=0.98, halo='auto', refit_scope='train', test_frac=0.25, s2_frac=0.5, stability_reps=0, xgb_params=None (600 trees, lr .05, depth 6, hist, early stop 50), seed=0. Full table with meanings in the class docstring.

v0.2 vocabulary extensions (all default-off; when off, the run — claims, report dict, printed report — is byte-identical to v0.1): le_cuts=False mirrors every ≥ cut as a ≤ twin, making low-side cells nameable and claimable (the duplicate prune switches from |r| to signed r so exact complements survive); band_conj=False admits same-column (x>=a)&(x<=b) pairs, making interior bands first-class atoms; n_path_harvest=0 with path_depth=3 harvests top-gain root-subpath conjunctions from the fitted engine's own trees (Yes branch → ≤; numeric features only; standard leaf grammar), diversified by path_per_set=3 so dominant structures cannot monopolize the harvest; core_dedup_r=None applies the dictionary's duplicate principle at core admission — one representative per near-duplicate family — without which a densified vocabulary floods the core with shadows whose S2 partial t's split and BH kills the whole family.

Tests

python tests/test_firewall.py     # verifier imports ⊆ stdlib+numpy, zero engine imports
python -m pytest tests/           # 35 contract + protocol + verifier-mutation tests
python tests/selftest.py          # T1-T7 acceptance ledger (17/17)

Deferred by design until the respective layers land: bundle-schema snapshots and renderer golden files (reporting layer), enforce-signature tests (refit mode), and the multi-version xgboost/lightgbm adapter matrix (CI env matrix).

Road to 1.0.0

• A schema_version field in the evidence bundle, honored by the verifier.
• enforce grows by keyword-only arguments from here; the positional surface is frozen at 0.9.0.
• The deferred snapshot/golden tests above.
• Semantic versioning from 0.9.0: breaking changes to the evidence-bundle schema or the public API happen only at a major version; 1.0.0 marks the freeze of both.

Guarantees, estimates, and caveats

• Controlled: the FDR of the claims ledger, by BH(q) over a single selection-conditional S2 pass. Exact: every #exact quantity is an arithmetic fact of the artifact (and sample) — structural zeros, masses, prices, off-rule bit-identity.
• Float32 is the write-back resolution: appended-tree coefficients are stored as float32 by the native format; certification tolerances (structural ≤ 1e-4, behavioral ≤ 1e-3) state this rather than hide it. Measured values are orders of magnitude below the gates.
• Estimates are labeled: holdout deltas carry CIs; the sieve's penumbra, toll bounds, spotlight, and M_C are plug-in quantities with disclosed proxies; ridge* is a hindsight benchmark for the frame-blind class, not a deployable model.
• The limits panel is non-removable: no proxy claim, no causal claim, no off-distribution claim, no fairness-of-outcomes claim — certified absence of named rule families in the file at the stated hash, and nothing more.
• refit_scope='train' re-uses S2 in the sieve's refit and carries a residual selection-optimism term (measured small); 's2' avoids it; both rows print.
• Verifier independence is a checked property, not a promise (see Tests).

Not in 0.9.0

lightgbm adapter; xgboost version matrix beyond 3.3.0; sealed PDF export (the HTML certificate binds to the same bundle); behavioral probe for involving clauses (structural only); refit surgery mode (excise only); monitor; vertical report packs; NaN-aware transported audit (R-07 declared instead).

Reproducibility

All stochastic steps are seeded (seed; house conventions: split rng 4000+seed, engine 9000+seed, stability replicates 31000+b). Given a seed, repeated runs reproduce the same report and the same certificate id up to timestamps. Runtime reference (single container CPU): full acceptance ledger ≈ 8 s; independent verification of the demo dossier ≈ 5 s; sieve on Adult (45,222 rows, P = 235, B = 8) ≈ 10 s.

Files

src/provable/                  adapters_xgb · calculus · policy · evidence · surface · sieve
verify/src/provable_verify/    the independent checker (single module)
tests/                         firewall · contracts · protocol · verifier mutations · selftest
dossier_demo/                  a real enforce dossier: evidence.json, certificate.md,
                               model.json, model_v2.json, MANIFEST.sha256, HOW_TO_VERIFY.txt

Citing

CITATION.cff ships in this repository. BibTeX:

@software{provable2026,
  author  = {Souihli, Oussama},
  title   = {provable: Exact audit, surgery, and certified discovery for tree ensembles},
  year    = {2026},
  version = {0.9.0},
  doi     = {10.5281/zenodo.21819947},
  url     = {https://provable.ml}
}

@misc{souihli2026calculus,
  author = {Souihli, Oussama},
  title  = {Every Interaction Has a Price: An Exact Calculus for Tree Ensembles},
  year   = {2026},
  doi    = {10.5281/zenodo.21819690}
}

@misc{souihli2026instrument,
  author = {Souihli, Oussama},
  title  = {Certified Discovery on Real Grams: an Instrument, its Limits, and its Laws},
  year   = {2026},
  doi    = {10.5281/zenodo.21819895}
}

@misc{souihli2026metrology,
  author = {Souihli, Oussama},
  title  = {Dark-Mass Metrology: Pricing What a Certified Model Does Not Know},
  year   = {2026},
  doi    = {10.5281/zenodo.21819925}
}

License: MIT.