Resources
Technical articles, industrial case studies, and tool documentation to help you get started with formal software verification.
Blog
An accessible introduction to bounded model checking — what it proves within a verification bound, how it differs from static analysis and testing, and why regulators are increasingly recommending it as part of the assurance case.
Full article coming soon — contact us to be notified.
ESBMC-Python identified a division-by-zero in the integer_squareroot helper of the Ethereum consensus specification; the fix was merged upstream as ethereum/consensus-specs PR #3600. Published at ACM SIGSOFT ISSTA 2024.
Full article coming soon — contact us to be notified.
In our SAS 2024 collaboration with engineers from Arm, ESBMC identified 23 additional property violations in the Realm Management Monitor on top of those already detected by CBMC, and contributed a confirmed memory-model fix upstream.
Full article coming soon — contact us to be notified.
How ESBMC-based formal verification integrates with ISO 26262 workflows — from ASIL-rated evidence generation to MISRA C compliance and AUTOSAR component verification — paired with our Tool Qualification & Certification Support service for the qualification artefacts your assessor expects.
Full article coming soon — contact us to be notified.
Large language models accelerate delivery but introduce security debt at scale. ESBMC-AI surfaces what the LLM missed and proposes candidate patches for engineer review — a formal-methods safety net for teams adopting LLMs in their development workflow.
Full article coming soon — contact us to be notified.
