Pular para o conteúdo principal
Verificação Formal de Software · ESBMC desde 2008

Prove.
Não apenas teste.

Usamos verificação formal, não apenas testes, para encontrar os bugs que outras ferramentas deixam passar e provar sua ausência em software de segurança crítica.

Nossos Serviços Ver Estudos de Caso

Estudos de caso publicados

Intel Arm Ethereum Foundation Rust Foundation AWS NVIDIA Chromium Dashboard

1.500%

Ganho de desempenho alcançado na verificação de firmware da Intel

23

Violações de propriedade adicionais que o ESBMC encontrou no firmware RMM da Arm (SAS 2024)

PR #3600

Correção nas consensus-specs do Ethereum incorporada upstream após nosso relatório com ESBMC-Python (ISSTA 2024)

F-1

Escrita fora dos limites no NVIDIA OpenSMA confirmada e corrigida upstream após nossa PoC de 2026

Por que verificação formal?

Testar é amostrar.
Verificação formal é prova.

Testes verificam os casos que você imagina. A verificação formal verifica toda entrada possível, incluindo o caso extremo de integer_squareroot que nosso relatório com ESBMC-Python apontou na especificação de consenso do Ethereum, os gargalos de verificação que bloquearam a análise de firmware da Intel e as 23 violações de propriedade adicionais que o ESBMC identificou no firmware RMM da Arm além daquelas que o CBMC já havia detectado.

O ESBMC usa solucionadores de Satisfatibilidade Módulo Teorias (SMT) para raciocinar matematicamente sobre o comportamento do seu código, produzindo seja uma prova de correção, seja um contraexemplo concreto que mostra exatamente como um bug pode ser disparado.

Saiba como o ESBMC funciona
integer_squareroot helper (Python) 
def integer_squareroot(n: uint64) -> uint64:
  x = n
  y = (x + 1) // 2  # ← overflows to 0 when n = 2⁶⁴ − 1
  while y < x:
    x = y                 # x becomes 0 after the overflow
    y = (x + n // x) // 2  # ← ZeroDivisionError: n // 0
  return x

# Input:  n = 2⁶⁴ − 1 (maximum uint64 value)
# Result: ZeroDivisionError, the unsigned integer overflows to 0,
#         then is used as the denominator of a division operation.
# ESBMC-Python: confirmed the bug and produced a counterexample trace.

Como ajudamos

Nossos Serviços

Consultoria em Verificação

Integre o ESBMC ao seu SDLC para provar formalmente a ausência de erros de execução em C, C++, Rust, Python, Solidity e mais.

Saiba mais

Auditoria de Segurança de Código

Análise profunda de código usando verificação limitada de modelos, produzimos prova matemática ou um contraexemplo concreto, não avisos heurísticos de análise estática.

Saiba mais

Reparo de Bugs Assistido por IA

O ESBMC-AI detecta e corrige automaticamente erros de memória, estouros e comportamento indefinido em código gerado por humanos e por LLMs. Integra-se ao VSCode e ao GitHub CI.

Saiba mais

Treinamentos e Workshops

Treinamento prático em métodos formais para equipes de engenharia, de introduções de meio dia a cursos sob medida de ESBMC com vários dias, presenciais ou remotos.

Saiba mais

Comprovado em produção

Estudos de Caso

Intel Semicondutor · Firmware

1.500%

ganho de desempenho na verificação

Verificação Formal Escalável de Firmware

Ler estudo de caso
Arm Hardware · Computação Confidencial

23

violações de propriedade adicionais encontradas

Protegendo a Arm Confidential Computing Architecture

Ler estudo de caso
Ethereum Foundation Blockchain · Python

PR #3600

correção incorporada upstream

Relatando um Bug em integer_squareroot na Especificação de Consenso

Ler estudo de caso
verify-rust-std project Ecossistema de código aberto · Rust

1 de 4

ferramentas de verificação listadas no projeto

ESBMC no Projeto verify-rust-std

Ler estudo de caso
NVIDIA OpenSMA Firmware de data center · C++23

F-1

escrita OOB corrigida upstream pela NVIDIA

Verificando o Firmware NVIDIA OpenSMA com ESBMC

Ler estudo de caso
AWS Neuron (NKI) Aceleradores de IA · Kernels em Python

2

novos bugs de divisão por zero no NKI reportados e corrigidos upstream pela AWS

Verificando Kernels NKI do AWS Neuron com ESBMC

Ler estudo de caso
vLLM Inferência de LLM · Python

6 de 7

descobertas alcançáveis pela CLI corrigidas upstream no vLLM

Verificando a Aritmética de Configuração do vLLM com ESBMC

Ler estudo de caso
Chromium Dashboard Infraestrutura de desenvolvimento · Python

3

de 7 issues reportadas no rastreador do Google corrigidas no upstream

Verificando o Chromium Dashboard do Google com ESBMC

Ler estudo de caso
AWS SDK for C++ · Base64 SDK de nuvem · C++

2 CVEs

problemas de segurança de memória corrigidos pela AWS no SDK 1.11.862

Dois CVEs de Segurança de Memória no Base64 do AWS SDK for C++

Ler estudo de caso
AWS SDK for C++ · DateTime SDK de nuvem · C++

PR #3896

dois bugs no parser DateTime corrigidos pela AWS no SDK 1.11.877

Dois Bugs no Parser DateTime do AWS SDK for C++

Ler estudo de caso

Setores que atendemos

Indústrias

Aeroespacial e Defesa

Verificação de Software Aéreo e Espacial

Verificação formal para certificação DO-178C, DO-330 e ARP4754A. Ajudamos a produzir evidências rigorosas que satisfazem os mais altos níveis de garantia.

DO-178CDO-330ARP4754ADO-254
Saiba mais

Automotivo

Garantia de Segurança Funcional

Evidências formais para conformidade com ISO 26262 ASIL-D. Verificamos firmware de ECU, software ADAS e componentes AUTOSAR em relação aos seus requisitos de segurança.

ISO 26262MISRA CAUTOSARSOTIF
Saiba mais

Semicondutor

Verificação de Firmware para Silício

Verificação formal para microcódigo de processadores, raiz de confiança, TEE e firmware de plataforma, aplicada em nossas colaborações publicadas com Intel e Arm.

Common CriteriaFIPS 140-3PSA CertifiedNIST 800-193
Saiba mais

Pronto para tornar seu software comprovadamente correto?

Agende uma conversa de descoberta gratuita de 30 minutos para discutir como a verificação formal pode funcionar para o seu projeto.

Agendar uma conversa de descoberta Ver nossos resultados