# Harmonic amplia Aristotle para verificar software e hardware

A empresa anunciou suporte a C e Verilog com provas verificadas por máquina; propriedades e pressupostos continuam sujeitos à revisão.

Autoria: Angelo Sebastião Silva Goncalves
Publicado: 2026-10-29T20:36:36.684Z
Revisado: 2026-10-29T20:36:36.684Z
URL canônica: https://nextags.com.br/news/harmonic-aristotle-verificacao-software-hardware/

A Harmonic anunciou, em 27 de outubro, uma ampliação do Aristotle para verificação de software em C e hardware em Verilog. Segundo a empresa, o sistema produz provas verificadas por máquina sobre propriedades especificadas, dentro dos pressupostos adotados. Isso não equivale a uma garantia geral de ausência de falhas.

O fluxo proposto identifica propriedades no código e distingue o que foi demonstrado, o que permanece sem prova e as hipóteses utilizadas. Engenheiros revisam os resultados antes de incorporá-los ao desenvolvimento. A cobrança é por consumo, com contratação empresarial; preço e disponibilidade brasileira não foram explicitados.

## Provas exigem especificação

Uma questão anterior à execução da prova é decidir o que precisa ser demonstrado. Na nota de pesquisa Towards Deriving Verification Properties, publicada no arXiv em março de 2019, Michael Winikoff identifica uma premissa recorrente dos métodos formais: as propriedades relevantes costumam ser tratadas como conhecidas ou já fornecidas durante o levantamento de requisitos.

O trabalho pergunta de onde essas propriedades vêm e propõe identificá-las sistematicamente. Esse recorte ajuda a separar duas atividades: formular o comportamento esperado de um sistema e demonstrar que esse comportamento atende a uma descrição lógica. A nota apresentada pelo pesquisador é uma proposta metodológica voltada à identificação das propriedades de verificação.

## Manutenção das provas

A revisão QED at Large, de Talia Ringer e outros pesquisadores, discute outra dimensão: o desenvolvimento e a manutenção de provas. O artigo, publicado em periódico em 2019 e depositado no arXiv em março de 2020, observa que projetos com provas verificadas por máquina passaram a alcançar escala comparável à de grandes projetos de software.

Segundo os autores, esse crescimento traz desafios próprios de engenharia. A revisão organiza fundamentos, automação, estrutura das provas e práticas de desenvolvimento; também ressalta que provas podem melhorar a compreensão das especificações e dos pressupostos de um programa. A organização das provas integra essa discussão. O levantamento reúne literatura sobre engenharia de provas de correção de programas.

Na análise editorial, a avaliação empresarial envolve o escopo efetivamente demonstrado, a revisão das hipóteses e a capacidade de manter as provas ao mudar o código em produção. Uma demonstração específica não sustenta, sozinha, uma promessa de qualidade para o sistema completo.

Vlad Tenev, cofundador da Harmonic, em retrato de 10 de setembro de 2025. Foto: [Pierce Larick/Wikimedia Commons](https://commons.wikimedia.org/wiki/File:Portrait_of_Vlad_Tenev.jpg), [CC BY-SA 4.0](https://creativecommons.org/licenses/by-sa/4.0/). Fotografia inteira redimensionada com margens e convertida para WebP; adaptação sob a mesma licença.

## Fontes

- [Harmonic](https://www.harmonic.fun/news/aristotle-software-hardware-verification/)
- [Winikoff](https://arxiv.org/abs/1903.04159)
- [Ringer e outros](https://arxiv.org/abs/2003.06458)

## Fontes
- [Harmonic](https://www.harmonic.fun/news/aristotle-software-hardware-verification/)
- [Winikoff](https://arxiv.org/abs/1903.04159)
- [Ringer e outros](https://arxiv.org/abs/2003.06458)
- [Origem da fotografia](https://commons.wikimedia.org/wiki/File:Portrait_of_Vlad_Tenev.jpg)
- [CC BY-SA 4.0](https://creativecommons.org/licenses/by-sa/4.0/)