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
PR #43794
três bugs de crash de CLI corrigidos no upstream do vLLM
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; três crashes de divisão por zero (--block-size 0, --hash-block-size 0, --max-model-len 0) foram confirmados e corrigidos no upstream na PR #43794, com três outras lacunas de validação de configuração reportadas e em aberto.
Ler estudo de caso completoChromium Dashboard
2026
2
de 10 achados confirmados e corrigidos no upstream pelo Google (PR #6451, PR #6452)
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; os mantenedores do chromium-dashboard no Google confirmaram e corrigiram dois dos achados no upstream nas PR #6451 e PR #6452.
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.