Service · Anchor offering
Tool Qualification &
Certification Support
ESBMC outputs only count as certification evidence if the tool itself is qualified for your assurance level. We build the qualification artefacts that support that argument — DO-330 kits, ISO 26262 Tool Confidence Level evidence, IEC 61508-aligned packages, and Common Criteria support — for review by your DER or functional-safety assessor.
The problem
A formal proof is not certification evidence on its own
Aerospace, automotive, rail, industrial-safety and medical regulators all require that any tool whose output is used as verification evidence is itself qualified to a level commensurate with the safety integrity of the software being verified. ESBMC is no different.
Without a qualification package, an ESBMC counterexample or proof is engineering insight — useful, but unlikely to be accepted at the safety assessment. Our role is to provide the qualification evidence your DER or assessor needs to consider.
Our approach
A qualification kit you can hand to your DER or assessor
We work alongside your safety engineers, certification managers, and DERs (or your ISO 26262 functional-safety manager) to produce the artefacts your assurance case needs — written in the language and structure that the regulator expects.
The package travels with your project. As ESBMC versions evolve, we maintain the configuration baseline and re-verify the qualification evidence so your safety case stays live.
Standards we address
Qualification scope
DO-178C / DO-330
Software Considerations in Airborne Systems (DO-178C) and the companion Software Tool Qualification Standard (DO-330). We help build the qualification artefacts supporting ESBMC outputs as qualified-tool evidence at DAL A through DAL E, subject to acceptance by your DER or assessor.
ISO 26262
Road vehicles — functional safety. We provide Tool Confidence Level (TCL) evidence per ISO 26262-8 §11, suitable for ASIL A through ASIL D software development tool qualification.
IEC 61508
Functional safety of electrical / electronic / programmable electronic safety-related systems. SIL-aligned tool qualification packages for industrial control, energy, and process safety.
EN 50128 / EN 50657
Railway applications — software for railway control / on-board software. Tool qualification evidence aligned with the standards' tool classification regime.
ISO/IEC 15408 (Common Criteria)
Formal verification supports the higher Evaluation Assurance Levels (EAL5+) typically required for secure-element, TEE, and root-of-trust firmware certification.
IEC 62304
Medical device software lifecycle. Tool qualification arguments tailored to the IEC 62304 software safety classification (Class A–C).
What you get
Deliverables
Tool Qualification Plan (TQP)
A formal plan covering ESBMC's intended use, operational context, and qualification evidence, structured to slot into your DO-178C plans (PSAC / SDP / SVP / SCMP / SQAP) or ISO 26262 safety case.
Tool Operational Requirements (TOR)
A precise, testable specification of what ESBMC does on your project, what its outputs mean, and how those outputs are used as verification evidence.
Tool Validation & Verification cases
Validation evidence that ESBMC behaves as specified in your operational environment, including configuration management, deterministic-build evidence, and known-issue tracking.
TCL classification rationale (ISO 26262)
A documented Tool Impact / Tool Error Detection analysis leading to a defensible Tool Confidence Level, with the supporting evidence required for ASIL D applicability.
Traceability matrix
Bi-directional traceability from your safety requirements to the formal properties verified by ESBMC and the resulting proofs or counterexamples.
DER / assessor liaison support
We can attend Stage of Involvement (SOI) reviews with your Designated Engineering Representative or independent assessor, and respond to clarifying questions on the ESBMC tool qualification evidence.
Why us
An assessor-credible evidentiary base
- ESBMC has been continuously developed and competition-validated since 2008, with 50+ awards across the SV-COMP and Test-Comp international competitions (TACAS/FASE 2012–2026).
- The same team has produced the canonical ESBMC publications (IEEE Transactions on Software Engineering 2011, ICSE'11 Distinguished Paper, ASE'24 Distinguished Paper, ASE'23 Most Influential Paper) — an unusually strong evidentiary base for a tool qualification argument.
- Lucas Cordeiro is Director of the Arm Centre of Excellence at the University of Manchester and a member of the EPSRC Peer Review Full College, with direct experience supporting industrial verification at Intel, Arm, and AWS-sponsored open-source efforts.
Note. This is a service offering. Cyber-Reasoning Consultancy (CRC) produces tool-qualification evidence packages for review by your Designated Engineering Representative, EASA / FAA / UK CAA representative, ISO 26262 Functional Safety Assessor, IEC 61508 assessor, or notified body. Admissibility decisions remain with the assessor — we do not act as the certifying authority and we do not warrant regulatory acceptance of any particular package. CRC is not an FAA Designated Engineering Representative, an EASA-listed agency, or an accredited certification body. Where required, we work alongside, and defer to, your nominated assessors.
Working toward DO-178C, ISO 26262, or IEC 61508 sign-off?
Tell us your target assurance level and the part of the lifecycle ESBMC will support. We'll scope the qualification package and pricing accordingly.