Formal verification toolkit for the certifiable ML pipeline.
Pure C99. Zero dynamic allocation. Certifiable for DO-178C, IEC 62304, and ISO 26262.
How do you prove a deployed ML model is exactly what you trained?
Traditional ML pipelines have no cryptographic chain of custody. You can't prove:
- The model was trained on the claimed data
- The quantization preserved accuracy within bounds
- The deployment bundle wasn't tampered with
- The inference outputs came from the correct model
- The monitoring ledger is intact
For safety-critical systems, "trust me" isn't good enough.
certifiable-verify provides cryptographic verification of the complete ML pipeline:
DATA ──────► TRAINING ──────► QUANT ──────► DEPLOY ──────► INFERENCE
│ │ │ │ │
▼ ▼ ▼ ▼ ▼
M_data ────► H_train ────► H_cert ────► R ────────► H_pred
│ │ │ │ │
└──────────────┴──────────────┴─────────────┴───────────────┘
│
CROSS-ARTIFACT BINDINGS
│
▼
VERIFICATION REPORT
Every hash, every binding, every chain — verified.
./certifiable-verify --artifacts ./model_v1.2.3/Verifies all cryptographic commitments in seconds:
- Data Merkle root matches training input
- Training chain hash is valid
- Quantization certificate within bounds
- Bundle attestation root correct
- Inference predictions hash matches
- Monitor ledger chain intact
- All cross-artifact bindings valid
./certifiable-verify --full-replay --artifacts ./model_v1.2.3/Re-runs the entire pipeline deterministically:
═══════════════════════════════════════════════════════════════
Certifiable Verify — Full Deterministic Replay
═══════════════════════════════════════════════════════════════
[1/6] Replaying data pipeline...
✓ 60,000 samples loaded
✓ Merkle root: MATCH
[2/6] Replaying training (10 epochs)...
✓ All weight hashes: MATCH
[3/6] Replaying quantization...
✓ Q16.16 weights: MATCH
✓ Error bounds: WITHIN CERTIFICATE
[4/6] Replaying bundle creation...
✓ Attestation root: MATCH
[5/6] Replaying inference (1000 samples)...
✓ All predictions: BIT-IDENTICAL
[6/6] Replaying monitor...
✓ Ledger chain: MATCH (847 entries)
═══════════════════════════════════════════════════════════════
FULL REPLAY VERIFICATION: PASS ✓
Original training date: July 15, 2026
Replay date: January 19, 2027
Bit-identical: YES
═══════════════════════════════════════════════════════════════
No other ML framework can do this.
| Module | Description | Status |
|---|---|---|
| provenance | Data Merkle verification | ✅ Complete |
| training | Training proof verification | ✅ Complete |
| quant | Quantization certificate verification | ✅ Complete |
| bundle | Bundle attestation verification | ✅ Complete |
| inference | Inference hash verification | ✅ Complete |
| ledger | Ledger chain verification | ✅ Complete |
| binding | Cross-artifact binding | ✅ Complete |
| replay | Full deterministic replay | ✅ Data replay (others stub) |
| report | JSON report generation | ✅ Complete |
10/10 test suites passing.
git clone https://github.com/williamofai/certifiable-verify.git
cd certifiable-verify
mkdir build && cd build
cmake ..
make
ctest --output-on-failure| Document | Purpose |
|---|---|
docs/CV-MATH-001.md |
Mathematical foundations |
docs/CV-STRUCT-001.md |
Data structure specification |
docs/requirements/SRS-001-PROVENANCE.md |
Data verification requirements |
docs/requirements/SRS-002-TRAINING.md |
Training verification requirements |
docs/requirements/SRS-003-QUANT.md |
Quantization verification requirements |
docs/requirements/SRS-004-BUNDLE.md |
Bundle verification requirements |
docs/requirements/SRS-005-INFERENCE.md |
Inference verification requirements |
docs/requirements/SRS-006-LEDGER.md |
Ledger verification requirements |
docs/requirements/SRS-007-BINDING.md |
Binding verification requirements |
docs/requirements/SRS-008-REPORT.md |
Report generation requirements |
{
"version": "1.0.0",
"mode": "hash_only",
"platform": "x86_64",
"timestamp": 1737302400,
"stages": [
{"stage": 0, "name": "data", "valid": true},
{"stage": 1, "name": "training", "valid": true},
{"stage": 2, "name": "quant", "valid": true},
{"stage": 3, "name": "deploy", "valid": true},
{"stage": 4, "name": "inference", "valid": true},
{"stage": 5, "name": "monitor", "valid": true}
],
"bindings": [
{"from": "data", "to": "training", "valid": true},
{"from": "training", "to": "quant", "valid": true},
{"from": "quant", "to": "deploy", "valid": true},
{"from": "deploy", "to": "inference", "valid": true},
{"from": "inference", "to": "monitor", "valid": true},
{"from": "deploy", "to": "monitor", "valid": true}
],
"pipeline_valid": true,
"report_hash": "a1b2c3d4..."
}| Project | Description |
|---|---|
| certifiable-data | Deterministic data pipeline |
| certifiable-training | Deterministic training engine |
| certifiable-quant | Deterministic quantization |
| certifiable-deploy | Deterministic model packaging |
| certifiable-inference | Deterministic inference engine |
| certifiable-monitor | Runtime drift detection |
Together, these projects provide a complete deterministic ML pipeline:
certifiable-data → certifiable-training → certifiable-quant → certifiable-deploy → certifiable-inference
↓
certifiable-monitor
↓
certifiable-verify
Dual Licensed:
- Open Source: GPL-3.0 — Free for open source projects
- Commercial: Available for safety-critical systems requiring certification support
See LICENSE for details.
Built on the Murray Deterministic Computing Platform (MDCP), UK Patent GB2521625.0.
The certifiable-* family implements deterministic computing primitives that enable bit-identical reproducibility across platforms — essential for formal verification of ML systems.
Built by SpeyTech in the Scottish Highlands.
William Murray — 30 years UNIX systems experience, Visiting Scholar at Heriot-Watt University.
Contact: william@fstopify.com — speytech.com
When regulators ask "prove it," we can.
Copyright © 2026 The Murray Family Innovation Trust. All rights reserved.