Skip to main content

Services

How we can help

End-to-end formal verification, led by the team that built ESBMC. From microcode and root-of-trust firmware to DO-330 tool qualification kits, we cover the spectrum of work that aerospace, automotive, and semiconductor teams need from a verification consultancy.

Track record

Published collaborations with Intel, Arm, AWS, the Ethereum Foundation, and the Rust Foundation — each evidenced by a published paper, official listing, or merged upstream artefact.

Research depth

Led by Prof. Lucas Cordeiro, creator of ESBMC, Director of the Arm Centre of Excellence at Manchester, EPSRC Peer Review College member, with 50+ awards at the SV-COMP and Test-Comp international competitions (2012–2026).

Tool pedigree

ESBMC is one of four verification tools listed in the model-checking/verify-rust-std book and has been continuously developed and competition-validated since 2008.

Anchor service · Sector-specific

Firmware & Silicon Verification

Semiconductor · TEE · Confidential Computing

Bounded model checking at scale on processor microcode, root-of-trust, TEE supervisors, and platform firmware — the same class of work demonstrated in our published Intel collaboration (190,000-LOC firmware verified in 8 hours via interval analysis) and our published Arm collaboration (Realm Management Monitor verification for the Armv9 Confidential Computing Architecture).

Learn more

Deliverables

  • Spec-driven harness generation
  • Memory-isolation & privilege-boundary properties
  • Verifier-level optimisations (interval analysis, VO-GCSE)
  • Cross-tool comparison (CBMC, Kani) where required

Pricing: Project-based

Anchor service · Sector-specific

Tool Qualification & Certification Support

Aerospace · Automotive · Industrial

Qualification artefacts and tool-confidence-level evidence supporting your DO-178C, DO-330, ISO 26262, and IEC 61508 assurance cases. We work alongside your safety engineers and DERs to integrate formal verification into the certification narrative — not just the engineering one. Admissibility decisions remain with your DER, EASA / FAA representative, or functional-safety assessor.

Learn more

Deliverables

  • DO-330 Tool Qualification Plan & Operational Requirements
  • ISO 26262 Tool Confidence Level (TCL) evidence
  • Tool Validation & Verification cases
  • Traceability from safety requirements to formal proofs

Pricing: Fixed-price per qualification package

Verification Consulting

Cross-sector

Embed ESBMC into your software development lifecycle to formally prove safety and security properties in C, C++, Rust, Python, Solidity, CUDA, Kotlin, and Java. We produce formal evidence packages anchored on the same techniques delivered in our Intel, Arm, and Ethereum case studies.

Learn more

Deliverables

  • Verification plan & property catalogue
  • ESBMC integration & CI/CD configuration
  • Formal evidence pack
  • Counterexample analysis reports

Pricing: Day-rate or project-based

Security Code Audit

Cross-sector

One-off deep formal analysis using bounded model checking. Unlike static analysis tools that produce heuristic warnings, every confirmed violation we report is backed by a concrete counterexample trace — reproducible end-to-end and ready for triage.

Learn more

Deliverables

  • Audit scope definition
  • ESBMC-based formal analysis
  • Severity-ranked findings with proof traces
  • Remediation guidance & re-verification

Pricing: Fixed-price (scoped per KLOC)

AI-Assisted Bug Repair

Cross-sector

ESBMC-AI helps detect potential memory errors, overflows, and undefined behaviour in human- and LLM-generated code, and proposes candidate patches for triage by your engineers. Intended to integrate with the CI/CD pipelines that regulated teams already feed from Vector, AdaCore, Wind River, and MathWorks toolchains.

Learn more

Deliverables

  • CI/CD pipeline integration
  • Automated detection & candidate-repair reports
  • Regression verification
  • Developer tooling setup (VSCode, GitHub Actions, GitLab)

Pricing: Retainer (monthly) or project-based

Training & Workshops

Cross-sector

Formal methods training for engineering teams, taught by Lucas Cordeiro, creator of ESBMC, with qualified associates as required. From half-day introductions to bespoke multi-day ESBMC courses, on-site or remote, adapted to your codebase, toolchain, and applicable safety standard.

Learn more

Deliverables

  • Tailored course material (DO-178C / ISO 26262 / Common Criteria streams available)
  • Hands-on ESBMC exercises on your representative code
  • Post-workshop support
  • Custom tooling guides for your CI

Pricing: Fixed-price per cohort

Not sure where to start?

Book a free 30-minute discovery call. We'll help you identify the right approach for your project, language, sector, and applicable safety or security standard.

Book a discovery call