Deterministic, certifiable model quantization for safety-critical systems.
Pure C99. Zero dynamic allocation. Certifiable for DO-178C, IEC 62304, and ISO 26262.
Standard quantization tools (TensorFlow Lite, ONNX quantizers) are black boxes:
- Error bounds unknown or unbounded
- No formal proof that quantized model preserves behavior
- Calibration statistics non-reproducible
- No audit trail linking original to quantized weights
For safety-critical systems, "approximately equivalent" isn't certifiable.
Read more: Fixed-Point Neural Networks: The Math Behind Q16.16
certifiable-quant provides provable quantization with formal error certificates:
Compute error bounds before quantization: overflow proofs, range propagation, operator norms.
Collect min/max statistics from representative data with coverage metrics and degenerate detection.
Quantize FP32→Q16.16 with formal error bounds and verify against theoretical limits.
Generate proof object with Merkle root linking analysis, calibration, and verification digests.
Result: A certificate proving the quantized model is within ε of the original, auditable forever.
All core modules complete — 7/7 test suites passing.
| Module | Description | Status |
|---|---|---|
| DVM Primitives | Fixed-point arithmetic with fault detection | ✅ |
| Analyze | Theoretical error bounds, overflow proofs | ✅ |
| Calibrate | Runtime statistics, coverage metrics | ✅ |
| Convert | FP32→Q16.16 with BatchNorm folding | ✅ |
| Verify | Check quantized values against bounds | ✅ |
| Certificate | Merkle-rooted proof generation | ✅ |
| Bit Identity | Cross-platform reproducibility tests | ✅ |
All project tasks are available as Makefile targets, and GitHub Actions CI uses
these to ensure that they are not stale. Documentation of the commands are
available via make help.
When building the project for the first time, run make deps.
To building everything (i.e. config, build, test), run make. Otherwise, use
individual Makefile targets as desired.
$ make help
Makefile Usage:
make <target>
Dependencies
deps Install project dependencies
Development
config Configure the build
build Build the project
Testing
test Run tests
Project Management
install Install the project
release Build release artifacts
Maintenance
clean Remove all build artifacts
Documentation
help Display this help100% tests passed, 0 tests failed out of 7
Total Test time (real) = 0.02 sec
#include "cq_types.h"
#include "analyze.h"
#include "calibrate.h"
#include "convert.h"
#include "verify.h"
#include "certificate.h"
ct_fault_flags_t faults = {0};
// 1. Analyze: compute theoretical 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);
// 2. Calibrate: collect runtime statistics
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);
// 3. Convert: quantize with error tracking
cq_convert_ctx_t convert;
cq_convert_init(&convert, CQ_FORMAT_Q16);
cq_quantize_tensor(fp32_weights, q16_weights, n, &convert, &faults);
// 4. Verify: check against 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);
// 5. Certificate: generate proof
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);
// Certificate contains Merkle root proving entire pipelineAll arithmetic operations use widening and saturation:
// CORRECT: Explicit widening
int64_t wide = (int64_t)a * (int64_t)b;
return dvm_round_shift_rne(wide, 16, &faults);
// FORBIDDEN: Raw overflow
return (a * b) >> 16; // Undefined behaviorRead more: From Proofs to Code: Mathematical Transcription in C
| Stage | Computes | Output |
|---|---|---|
| Analyze | ε₀ (entry error), εₗ (layer error), Lipschitz bounds | cq_analysis_digest_t |
| Calibrate | min/max, coverage %, degenerate flags | cq_calibration_digest_t |
| Convert | Actual quantized values | Quantized tensors |
| Verify | Pass/fail against theoretical bounds | cq_verify_digest_t |
| Certificate | Merkle root of all digests | cq_certificate_t |
Entry error for Q16.16:
ε₀ = 2^(-f-1) = 2^(-17) ≈ 7.6 × 10⁻⁶
Layer error propagation:
ε_{ℓ+1} = ρ_ℓ · ε_ℓ + δ_ℓ
Where ρ_ℓ is the Lipschitz constant (operator norm) and δ_ℓ is the layer's quantization error.
Read more: Closure, Totality, and the Algebra of Safe Systems
Every operation signals faults without silent failure:
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;typedef struct {
uint32_t version; /* Format version */
uint32_t format; /* CQ_FORMAT_Q16, etc. */
cq_hash_t analysis_digest; /* H(analysis results) */
cq_hash_t calibration_digest; /* H(calibration stats) */
cq_hash_t verification_digest; /* H(verification results) */
cq_hash_t merkle_root; /* Root of all digests */
int32_t total_error_bound; /* ε_total in Q16.16 */
uint8_t all_checks_passed; /* Global pass/fail */
} cq_certificate_t;| Module | Tests | Coverage |
|---|---|---|
| Analyze | 30 | Overflow proofs, range propagation, norms |
| Bit Identity | 9 | RNE patterns, SHA-256 vectors, cross-platform |
| Calibrate | 28 | Statistics, coverage, degenerate handling |
| Certificate | 27 | Builder, Merkle, serialization, roundtrip |
| Convert | 21 | RNE quantization, BatchNorm folding, dyadic |
| Primitives | 13 | Arithmetic, saturation, overflow safety |
| Verify | 22 | Bound checking, L∞ norm, contract validation |
Total: 150 tests
- CQ-MATH-001.md — Mathematical foundations (error theory)
- CQ-STRUCT-001.md — Data structure specifications
- docs/requirements/ — SRS documents:
- SRS-001-ANALYZE.md
- SRS-002-CALIBRATE.md
- SRS-003-CONVERT.md
- SRS-004-VERIFY.md
- SRS-005-CERTIFICATE.md
| 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 |
Together, these projects provide a complete deterministic ML pipeline for safety-critical systems:
certifiable-data → certifiable-training → certifiable-quant → certifiable-deploy → certifiable-inference
IEC 62304 Class C requires traceable, validated transformations. "We quantized it and it still works" is not certifiable.
Read more: IEC 62304 Class C: What Medical Device Software Actually Requires
ISO 26262 ASIL-D demands provable error bounds. Unbounded quantization error is a safety hazard.
Read more: ISO 26262 and ASIL-D: The Role of Determinism
DO-178C Level A requires complete requirements traceability. Every weight transformation must be auditable.
Read more: DO-178C Level A Certification: How Deterministic Execution Can Streamline Certification Effort
This is the first ML quantization tool designed from the ground up for safety-critical certification.
Want to understand the engineering principles behind certifiable-quant?
Fixed-Point Arithmetic:
- Fixed-Point Neural Networks: The Math Behind Q16.16
- From Proofs to Code: Mathematical Transcription in C
- Closure, Totality, and the Algebra of Safe Systems
Determinism & Reproducibility:
Safety-Critical Foundations:
Production ML Architecture:
This implementation is designed to support certification under:
- DO-178C (Aerospace software)
- IEC 62304 (Medical device software)
- ISO 26262 (Automotive functional safety)
- IEC 61508 (Industrial safety systems)
For compliance packages and certification assistance, contact below.
We welcome contributions from systems engineers working in safety-critical domains. See CONTRIBUTING.md.
Important: All contributors must sign a Contributor License Agreement.
Dual Licensed:
- Open Source: GNU General Public License v3.0 (GPLv3)
- Commercial: Available for proprietary use in safety-critical systems
For commercial licensing and compliance documentation packages, contact below.
This implementation is built on the Murray Deterministic Computing Platform (MDCP), protected by UK Patent GB2521625.0.
MDCP defines a deterministic computing architecture for safety-critical systems, providing:
- Provable execution bounds
- Resource-deterministic operation
- Certification-ready patterns
- Platform-independent behavior
Read more: MDCP vs. Conventional RTOS
For commercial licensing inquiries: william@fstopify.com
Built by SpeyTech in the Scottish Highlands.
30 years of UNIX infrastructure experience applied to deterministic computing for safety-critical systems.
Patent: UK GB2521625.0 - Murray Deterministic Computing Platform (MDCP)
Contact:
William Murray
william@fstopify.com
speytech.com
More from SpeyTech:
Building deterministic AI systems for when lives depend on the answer.
Copyright © 2026 The Murray Family Innovation Trust. All rights reserved.