Comprovado em produção
Estudos de Caso
O ESBMC foi aplicado a firmware, infraestrutura de blockchain e software de sistemas em algumas das principais organizações de tecnologia do mundo. Veja o que encontramos, e o que isso significou.
Intel
2021–2025
1.500%
aceleração de verificação
Semicondutores · Firmware
Verificação Formal Escalável de Firmware
Em um padrão de código de firmware representativo da Intel, nossa otimização VO-GCSE reduziu o tempo de verificação do ESBMC de 105 segundos para menos de 7 segundos; a análise de intervalos tornou então o firmware Core Power Management de 190.000 LOC da Intel verificável em 8 horas (contra um timeout de 3 dias).
Ler estudo de caso completoArm
2022–2024
23
violações de propriedade adicionais encontradas
Hardware · Computação Confidencial
Protegendo a Arm Confidential Computing Architecture
Em uma colaboração no SAS 2024 com engenheiros da Arm, o ESBMC identificou 23 violações de propriedade adicionais no firmware Realm Management Monitor além daquelas já detectadas pelo CBMC, fortalecendo a linha de base de garantia da implementação RMM publicada.
Ler estudo de caso completoEthereum Foundation
2023–2024
PR #3600
correção integrada no upstream
Blockchain · Python
Relatando um Bug em integer_squareroot na Especificação de Consenso do Ethereum
Usando o ESBMC-Python, o primeiro verificador de código Python baseado em BMC, identificamos uma divisão por zero no auxiliar integer_squareroot da especificação de consenso do Ethereum. A correção foi integrada ao upstream como ethereum/consensus-specs PR #3600. Publicado na ACM SIGSOFT ISSTA 2024.
Ler estudo de caso completoverify-rust-std project
2024–2026
1 de 4
ferramentas de verificação listadas no livro verify-rust-std
Ecossistema open-source · Rust
ESBMC no Projeto verify-rust-std
Vencemos a trilha Tool Applications da competição de verificação da biblioteca padrão do Rust patrocinada pela AWS. O ESBMC (via GOTO Transcoder) é agora uma das quatro ferramentas de verificação listadas no livro model-checking/verify-rust-std, ao lado de Kani, VeriFast e Flux, e roda no fluxo de CI do projeto.
Ler estudo de caso completoNVIDIA OpenSMA
2026
F-1
escrita OOB confirmada e corrigida no upstream pela NVIDIA
Firmware de data center · C++23
Verificando o Firmware NVIDIA OpenSMA com ESBMC
Em uma PoC verificando ~30 módulos C++23 de produção do firmware open-source MCXN556S System Management Agent da NVIDIA, o ESBMC identificou 17 achados distintos, incluindo uma escrita fora dos limites de Tier-A no validador MCTP que a equipe OpenSMA da NVIDIA confirmou e corrigiu no upstream em 2026-05-11. 22+ issues do frontend do ESBMC foram integradas ao longo do trabalho.
Ler estudo de caso completoAWS Neuron (NKI)
2026
2
novos bugs de divisão por zero em nki-samples reportados pela PoC e corrigidos pela AWS
Aceleradores de IA · Kernels Python
Verificando Kernels NKI do AWS Neuron com ESBMC
Uma PoC reproduzível mostrando que kernels do AWS Neuron Kernel Interface (NKI) para Trainium e Inferentia podem ser verificados estaticamente pelo frontend Python do ESBMC sem hardware Neuron. 19 kernels portam para uma única biblioteca de stub de ~865 LoC, 11 de 13 alvos simbólicos carregam certificados de completude por k-induction, e a PoC reportou dois novos bugs de divisão por zero que a AWS confirmou e corrigiu no upstream (nki-samples PR #126 e commit bb513ac), além de redescobrir o bug de formato do matmul da PR #74 em ~2 segundos.
Ler estudo de caso completovLLM
2026
6 de 7
descobertas alcançáveis pela CLI corrigidas no upstream do vLLM (PR #43794, PR #44070)
Inferência de LLM · Python
Verificando a Aritmética de Configuração do vLLM com ESBMC
Uma PoC reproduzível aplicando o frontend Python do ESBMC à aritmética de inteiros e índices do vLLM, o motor de inferência de LLM de alto throughput. Em 31 alvos escalonados (~4 min de ponta a ponta), o ESBMC revelou sete defeitos alcançáveis pela CLI; seis foram confirmados e corrigidos no upstream, três crashes de divisão por zero (--block-size 0, --hash-block-size 0, --max-model-len 0) na PR #43794 e dois defeitos de aceitação silenciosa na PR #44070, restando uma lacuna em aberto. Outra descoberta, apenas programática, foi corrigida na PR #44207.
Ler estudo de caso completoChromium Dashboard
2026
3
de 7 issues reportadas no rastreador do Google corrigidas no upstream (PR #6451, PR #6452, PR #6656)
Infraestrutura de desenvolvimento · Python
Verificando o Chromium Dashboard do Google com ESBMC
Uma PoC reproduzível aplicando o frontend Python do ESBMC ao chromium-dashboard, o backend em Google App Engine por trás do Chrome Platform Status. Em 48 alvos em cinco tiers (menos de 30s de ponta a ponta), o ESBMC confirmou dez achados de validação de API e provou formalmente dois invariantes de segurança; sete achados foram reportados como issues no rastreador público do Google e os mantenedores do chromium-dashboard corrigiram três delas no upstream nas PR #6451, PR #6452 e PR #6656.
Ler estudo de caso completoAWS SDK for C++ · Base64
2026
2 CVEs
problemas de segurança de memória corrigidos pela AWS (CVE-2026-19642, CVE-2026-19643)
SDK de nuvem · C++
Dois CVEs de Segurança de Memória no Base64 do AWS SDK for C++
Verificamos com o ESBMC o decodificador Base64 escrito à mão do AWS SDK for C++, conduzindo-o com entradas simbólicas em vez de strings de teste individuais. A análise revelou comportamento fora dos limites na aritmética de tamanho do decodificador, alcançável a partir de uma classe de entradas bem formadas. A AWS publicou o boletim de segurança 2026-080 para CVE-2026-19642 (escrita fora dos limites) e CVE-2026-19643 (leitura fora dos limites), ambos de severidade média e corrigidos no SDK 1.11.862.
Ler estudo de caso completoAWS SDK for C++ · DateTime
2026
PR #3896
dois bugs no parser DateTime confirmados e corrigidos pela AWS no SDK 1.11.877
SDK de nuvem · C++
Dois Bugs no Parser DateTime do AWS SDK for C++
De volta ao mesmo SDK, verificamos com o ESBMC seus parsers de timestamp RFC822, ISO-8601 e ISO-8601 Basic. Dois defeitos apareceram: campos guiados por delimitador acumulavam dígitos sem limite, estourando seus acumuladores int (comportamento indefinido), e datas fora da faixa eram convertidas sem verificação e devolvidas a quem chamou como parsing bem-sucedido. A AWS confirmou os dois, incorporou nosso patch de largura de campo e publicou a correção no PR #3896 (SDK 1.11.877) com 12 novos testes de regressão.
Ler estudo de caso completoSeu projeto pode ser o próximo
Entre em contato para conversar sobre como a verificação formal pode funcionar para sua base de código, linguagem e norma de segurança.