Certifiable Quant

Standard quantization tools treat model compression as an optimisation problem: shrink the weights, benchmark accuracy, ship it. For most applications, that’s fine. For safety-critical systems—where a misclassified obstacle or miscalculated dosage can cost lives—“approximately equivalent” isn’t certifiable.

certifiable-quant provides provable FP32→Q16.16 quantization with formal error bounds and cryptographic audit trails.

View on GitHub

The Problem with Black-Box Quantization

When you run a neural network through TensorFlow Lite or an ONNX quantizer, you get a smaller model. What you don’t get:

• Error bounds: How far can the quantized output deviate from the original?
• Reproducibility: Will the same input produce identical output on different hardware?
• Audit trail: Can you prove, years later, which original model produced this quantized version?

For DO-178C Level A aerospace software, IEC 62304 Class C medical devices, or ISO 26262 ASIL-D automotive systems, these aren’t nice-to-haves. They’re certification requirements.

How certifiable-quant Works

The pipeline has five stages, each producing a cryptographic digest that feeds into a final Merkle-rooted certificate.

1. Analyze

Before touching any weights, compute theoretical error bounds:

cq_analysis_ctx_t analysis;
cq_analysis_init(&analysis, num_layers);
cq_compute_weight_range(weights, n, &w_min, &w_max);
cq_compute_overflow_proof(w_max, x_max, n, &overflow_proof);
cq_analysis_digest_generate(&analysis, &analysis_digest);

This establishes the entry error (ε₀ = 2⁻¹⁷ for Q16.16) and computes Lipschitz constants for layer-by-layer error propagation.

2. Calibrate

Collect runtime statistics from representative data:

cq_tensor_stats_t stats;
cq_tensor_stats_init(&stats, CQ_FORMAT_Q16);
for (int i = 0; i < num_samples; i++) {
    cq_tensor_stats_update(&stats, activations[i], size);
}
cq_calibration_digest_generate(&calib, &calib_digest);

The calibration module tracks min/max ranges, coverage percentages, and flags degenerate distributions that might indicate insufficient calibration data.

3. Convert

Quantize with explicit fault detection:

cq_convert_ctx_t convert;
cq_convert_init(&convert, CQ_FORMAT_Q16);
cq_quantize_tensor(fp32_weights, q16_weights, n, &convert, &faults);

All arithmetic uses widening multiplication and Round-to-Nearest-Even (RNE) rounding—no silent overflow, no undefined behaviour.

4. Verify

Check quantized values against theoretical bounds:

cq_verify_ctx_t verify;
cq_verify_init(&verify, &analysis);
bool passed = cq_verify_tensor(q16_weights, &analysis.contracts[layer], &verify);
cq_verify_digest_generate(&verify, &verify_digest);

If any value exceeds its computed bound, verification fails. No silent degradation.

5. Certificate

Generate the final proof object:

cq_certificate_builder_t builder;
cq_certificate_builder_init(&builder);
cq_certificate_builder_set_analysis(&builder, &analysis_digest);
cq_certificate_builder_set_calibration(&builder, &calib_digest);
cq_certificate_builder_set_verification(&builder, &verify_digest);

cq_certificate_t cert;
cq_certificate_build(&builder, &cert, &faults);

The certificate contains a Merkle root linking all three digests. Years later, you can prove exactly which analysis, calibration, and verification produced this quantized model.

Error Bound Theory

Q16.16 uses 16 fractional bits, giving an entry error of:

ε₀ = 2^(-f-1) = 2^(-17) ≈ 7.6 × 10⁻⁶

Error propagates through layers according to:

ε_{ℓ+1} = ρ_ℓ · ε_ℓ + δ_ℓ

Where ρ_ℓ is the layer’s Lipschitz constant (operator norm) and δ_ℓ is the layer’s quantization error. The analysis module computes these bounds before conversion begins—if the theoretical maximum error exceeds tolerance, you know before wasting compute on quantization.

The Fault Model

Every operation signals faults explicitly:

typedef struct {
    uint32_t overflow    : 1;  /* Saturated high */
    uint32_t underflow   : 1;  /* Saturated low */
    uint32_t div_zero    : 1;  /* Division by zero */
    uint32_t domain      : 1;  /* Invalid input */
    uint32_t precision   : 1;  /* Precision loss detected */
} ct_fault_flags_t;

No silent failures. If something goes wrong, the fault flags tell you what and where.

Test Coverage

All core modules are complete with 150 tests across 7 test suites:

Part of a Complete Pipeline

certifiable-quant is one component of a deterministic ML ecosystem:

certifiable-data → certifiable-training → certifiable-quant → certifiable-deploy → certifiable-inference

Each project maintains the same principles: pure C99, zero dynamic allocation, formal error tracking, and cryptographic audit trails. Together, they provide end-to-end traceability from training data through deployed inference.

When You Need This

Medical devices: IEC 62304 Class C requires traceable, validated transformations. “We quantized it and it still works” isn’t evidence.

Autonomous vehicles: ISO 26262 ASIL-D demands provable error bounds. Unbounded quantization error is a safety hazard.

Aerospace: DO-178C Level A requires complete requirements traceability. Every weight transformation must be auditable.

If your model makes decisions that affect human safety, black-box quantization creates certification risk. certifiable-quant is designed to address that gap.

Getting Started

git clone https://github.com/williamofai/certifiable-quant
cd certifiable-quant
mkdir build && cd build
cmake ..
make
make test

Expected output:

100% tests passed, 0 tests failed out of 7
Total Test time (real) = 0.02 sec

Documentation

The repository includes formal documentation suitable for certification evidence:

• CQ-MATH-001.md — Mathematical foundations and error theory
• CQ-STRUCT-001.md — Data structure specifications
• SRS documents — Software Requirements Specifications for each module

License

Dual licensed under GPLv3 (open source) and commercial terms for proprietary safety-critical systems. The implementation builds on the Murray Deterministic Computing Platform (UK Patent GB2521625.0).

For teams building safety-critical ML systems, certifiable-quant provides the formal rigour that certification demands. As with any architectural approach, suitability depends on system requirements, risk classification, and regulatory context.

View on GitHub · Request Technical Brief