Serviços
Como podemos ajudar
Verificação formal de ponta a ponta, conduzida pela equipe que construiu o ESBMC. De microcódigo e firmware de raiz de confiança a kits de qualificação de ferramentas DO-330, cobrimos todo o espectro de trabalho que equipes aeroespaciais, automotivas e de semicondutores precisam de uma consultoria em verificação.
Histórico comprovado
Colaborações publicadas com Intel, Arm, AWS, a Ethereum Foundation e a Rust Foundation; cada uma evidenciada por um artigo publicado, listagem oficial ou artefato incorporado upstream.
Profundidade em pesquisa
Conduzida pelo Prof. Lucas Cordeiro, criador do ESBMC, Diretor do Arm Centre of Excellence em Manchester, membro do EPSRC Peer Review College, com mais de 50 prêmios nas competições internacionais SV-COMP e Test-Comp (2012–2026).
Linhagem da ferramenta
O ESBMC é uma das quatro ferramentas de verificação listadas no livro model-checking/verify-rust-std e vem sendo continuamente desenvolvido e validado em competições desde 2008.
Serviço âncora · Específico por setor
Verificação de Firmware e Silício
Semicondutores · TEE · Computação Confidencial
Bounded model checking em escala sobre microcódigo de processador, raiz de confiança, supervisores de TEE e firmware de plataforma, a mesma classe de trabalho demonstrada em nossa colaboração publicada com a Intel (190.000 LOC de firmware verificados em 8 horas via análise de intervalos) e em nossa colaboração publicada com a Arm (verificação do Realm Management Monitor para a Armv9 Confidential Computing Architecture).
Saiba maisEntregáveis
- Geração de harness orientada por especificação
- Propriedades de isolamento de memória e de fronteira de privilégio
- Otimizações no nível do verificador (análise de intervalos, VO-GCSE)
- Comparação entre ferramentas (CBMC, Kani) quando necessário
Preço: Por projeto
Serviço âncora · Específico por setor
Apoio à Qualificação de Ferramentas e Certificação
Aeroespacial · Automotivo · Industrial
Artefatos de qualificação e evidências de nível de confiança da ferramenta que sustentam seus casos de garantia DO-178C, DO-330, ISO 26262 e IEC 61508. Trabalhamos lado a lado com seus engenheiros de segurança e DERs para integrar a verificação formal à narrativa de certificação, e não apenas à de engenharia. As decisões de admissibilidade permanecem com seu DER, representante da EASA / FAA ou avaliador de segurança funcional.
Saiba maisEntregáveis
- Plano de Qualificação de Ferramenta e Requisitos Operacionais DO-330
- Evidência de Tool Confidence Level (TCL) da ISO 26262
- Casos de Validação e Verificação de Ferramenta
- Rastreabilidade dos requisitos de segurança às provas formais
Preço: Preço fixo por pacote de qualificação
Consultoria em Verificação
Multissetorial
Incorpore o ESBMC ao seu ciclo de desenvolvimento de software para provar formalmente propriedades de segurança em C, C++, Rust, Python, Solidity, CUDA, Kotlin e Java. Produzimos pacotes de evidência formal ancorados nas mesmas técnicas entregues em nossos estudos de caso com Intel, Arm e Ethereum.
Saiba maisEntregáveis
- Plano de verificação e catálogo de propriedades
- Integração do ESBMC e configuração de CI/CD
- Pacote de evidência formal
- Relatórios de análise de contraexemplos
Preço: Diária ou por projeto
Auditoria de Segurança de Código
Multissetorial
Análise formal profunda pontual usando bounded model checking. Ao contrário das ferramentas de análise estática que produzem avisos heurísticos, cada violação confirmada que reportamos é respaldada por um traço concreto de contraexemplo, reproduzível de ponta a ponta e pronto para triagem.
Saiba maisEntregáveis
- Definição do escopo da auditoria
- Análise formal baseada em ESBMC
- Achados ordenados por severidade com traços de prova
- Orientação de correção e reverificação
Preço: Preço fixo (escopado por KLOC)
Reparo de Bugs Assistido por IA
Multissetorial
O ESBMC-AI ajuda a detectar possíveis erros de memória, estouros e comportamento indefinido em código gerado por humanos e por LLMs, e propõe patches candidatos para triagem por seus engenheiros. Projetado para integrar-se aos pipelines de CI/CD que equipes reguladas já alimentam a partir das toolchains da Vector, AdaCore, Wind River e MathWorks.
Saiba maisEntregáveis
- Integração ao pipeline de CI/CD
- Relatórios automatizados de detecção e reparo candidato
- Verificação de regressão
- Configuração de ferramentas para desenvolvedores (VSCode, GitHub Actions, GitLab)
Preço: Retainer (mensal) ou por projeto
Treinamentos e Workshops
Multissetorial
Treinamento em métodos formais para equipes de engenharia, ministrado por Lucas Cordeiro, criador do ESBMC, com associados qualificados conforme necessário. De introduções de meio dia a cursos ESBMC sob medida de vários dias, presenciais ou remotos, adaptados ao seu código, à sua toolchain e ao padrão de segurança aplicável.
Saiba maisEntregáveis
- Material de curso personalizado (trilhas DO-178C / ISO 26262 / Common Criteria disponíveis)
- Exercícios práticos de ESBMC sobre seu código representativo
- Suporte pós-workshop
- Guias de ferramentas customizados para seu CI
Preço: Preço fixo por turma
Sem saber por onde começar?
Agende uma reunião gratuita de descoberta de 30 minutos. Vamos ajudá-lo a identificar a abordagem certa para seu projeto, linguagem, setor e padrão de segurança ou de segurança da informação aplicável.