BATool is a research and audit tool. It is not a security boundary, safety guarantee, or compliance system. Use is entirely at your own risk. The authors and contributors accept no warranty, no liability, and no support obligations. Issues, PRs, and inquiries may be ignored or left unanswered.
BATool is an offline, fail-closed verifier for JSONL event logs. It emits:
- a deterministic, machine-readable certificate (JSON), and
- a deterministic, human-readable summary (text),
while separating claims (supported by the observed log) from non-claims (what cannot be supported, and why).
- Code and tooling: Apache-2.0 (see
LICENSEandNOTICE) - TeX sources under
paper/: CC-BY-4.0 (seepaper/LICENSEand file headers)
uv venv
uv pip install -e ./verifier
batool verify --input ./examples/ok_run/events.jsonl --out /tmp/certificate.json --human /tmp/summary.txtpython -m venv .venv
. .venv/bin/activate
pip install -e ./verifier
batool verify --input ./examples/ok_run/events.jsonl --out /tmp/certificate.json --human /tmp/summary.txtVERIFIED: no reject/undecidable triggers, and at least one claim is made.UNDECIDABLE: missing data or ambiguity (for example missing END events or clock skew beyond tolerance).REJECT: schema violations, inconsistent run_id, duplicate event_id, tamper mismatch, or strict-mode failures.
Exit codes: 0 VERIFIED, 1 UNDECIDABLE, 2 REJECT.
- Claims are explicitly supported by the observed data under this tool's validation rules.
- Non-claims explain what could not be supported, and why.
This tool does not infer causality. It performs telemetry-visible checks and heuristic aggregation only.
It prefers UNDECIDABLE / REJECT over guessing.
Use --strict to treat any clock decrease or missing END as REJECT. This is more conservative and intended for high-integrity pipelines.
BATool Verification Summary
Verdict: VERIFIED
Run ID: run-ok-001
Input Digest (sha256, KEYSORT_UTF8): 7f2b...
Claims:
- useful_compute_floor: 5 steps
- dominant_time_component: ALLREDUCE_DOMINANT (evidence=high)
- integrity: OK (contract_ok=true)
Non-claims:
- none
BATool implements a reduced log-checking protocol and a minimal certificate format. It does not implement the full statistical guarantees or cryptographic integrity models described in the following references.
- TLUC: https://doi.org/10.5281/zenodo.18051330
- SDC: https://doi.org/10.5281/zenodo.18050287
- MCCBE: https://doi.org/10.5281/zenodo.18057956
Not implemented (examples):
- confidence sequences or coverage-in-time proofs
- cryptographic authenticity or secure log signatures
- power/cooling estimators or hardware trust anchors
See docs/ for:
- certificate format (
docs/CERTIFICATE_FORMAT.md) - threat model (
docs/THREAT_MODEL.md) - versioning (
docs/VERSIONING.md) - reproducibility steps (
docs/REPRODUCIBILITY.md)