---
title: "Harmonic estende o Aristotle à verificação formal de software e hardware"
url: https://dailyjournal.news/news/2026-10-27/harmonic-lanca-ferramenta-de-ia-para-verificacao-automatica-de-codigo
published: 2026-10-27T16:41:07.901312+00:00
updated: 2026-10-27T17:10:38.018+00:00
categories: ["technology"]
source_count: 2
outlet_count: 0
language: pt-BR
publisher: "Daily Journal"
---

# Harmonic estende o Aristotle à verificação formal de software e hardware

A Harmonic estendeu o Aristotle à verificação formal de software em C e de hardware em Verilog, com provas matemáticas de que propriedades especificadas valem para todas as entradas possíveis de um sistema definido.

## Pontos principais

- A Harmonic afirma que, em C, o Aristotle verifica software contra requisitos especificados, incluindo corretude funcional e a ausência de certas classes de comportamento indefinido.
- Em Verilog, a Harmonic afirma que o Aristotle faz verificação lógica total de propriedades de caminho de controle, como liveness e safety, e de propriedades matemáticas de caminho de dados.
- Segundo a empresa, o Aristotle propõe propriedades a partir do código e informa quais provou, quais não provou e as premissas de cada prova.
- A Harmonic descreve um fluxo em que engenheiros revisam essas propriedades, as incluem no repositório e rodam o Aristotle em CI a cada commit, para que o que foi provado continue provado.
- A Harmonic informa que o Aristotle está disponível desde hoje, com preço por consumo no modo self-serve; os planos enterprise têm preço por volume, suporte dedicado e implantação on-prem ou em private cloud.
- A Harmonic não divulga métricas de desempenho nem clientes nomeados.

A Harmonic anunciou que o Aristotle, usado até então em matemática de pesquisa, passa a fazer verificação formal de software e hardware, começando por código em C e designs em Verilog. Segundo a empresa, o código gerado por IA já é escrito mais rápido do que as equipes conseguem revisar, e revisão e testes examinam só parte dos comportamentos possíveis. A verificação formal, ao contrário, prova se as propriedades especificadas valem para todas as entradas possíveis de um sistema definido.

## Fontes

- [@tachim: Starting today, Aristotle can verify C code including ~~memory safety~~, and control- and data-path properties of Verilog designs! We’ve started with bytes and electrons, and this …](https://x.com/tachim/status/2115119593006272569) (2026-10-27)
- [@HarmonicMath: We’re bringing Aristotle to code.](https://x.com/HarmonicMath/status/2115118879127351586) (2026-10-27)

---

Publicado por Daily Journal. Versão HTML: https://dailyjournal.news/news/2026-10-27/harmonic-lanca-ferramenta-de-ia-para-verificacao-automatica-de-codigo