Harmonic extends its Aristotle AI to formal verification of C software and Verilog chip designs

Harmonic, the AI startup co-founded by Robinhood chief executive Vlad Tenev, said on 27 October 2026 that its Aristotle system is moving beyond mathematical proofs into software and hardware verification. The first two languages supported are C, for software, and Verilog, for chip designs.

What Aristotle now checks

Aristotle is built on machine-checked proofs, and Harmonic says the goal is to show that specified properties hold for every possible input within a defined system, rather than sampling behaviour through tests or code review. For C, the company says Aristotle can verify code against stated requirements, including functional correctness and the absence of some classes of undefined behaviour. For Verilog, it covers control-path properties such as safety and liveness as well as mathematical properties of data paths.

The proposed workflow has four steps. Aristotle suggests properties based on the code, then reports which ones it managed to prove, which it did not, and the assumptions each proof depends on. Engineers review those properties and commit them to the repository, after which Aristotle can run in continuous integration so the proofs are re-checked on every commit.

Early results cited by the company

Harmonic gives two examples. At chip company Tensordyne, it says Aristotle found bugs up to 110,000 cycles deep in the block the team considered the hardest to verify. On LibTomMath, an open-source big-number library used by Tcl and Dropbear SSH, the company says Aristotle fixed three bugs and sped up modular exponentiation by 31 to 38 percent in its own benchmarks, with the faster code proved against the same specification. Reuters also reports that the DIII-D fusion facility in the US said Aristotle rebuilt part of its reactor-control software in four hours from a research paper and a short prompt.

These results come from the company and its users and have not been independently reproduced.

Why it matters

Formal verification has long been costly and largely confined to specialists, notably in chip design and safety-critical software. Harmonic argues that the growing volume of AI-generated code makes review a weak point, and that machine-checked proofs can fill part of that gap. Chief executive Tudor Achim says verification offers a new way to identify defects and vulnerabilities.

Aristotle is available now at aristotle.harmonic.fun with self-serve, usage-based pricing, and enterprise plans add volume pricing, dedicated support and on-premises or private-cloud deployment. The announcement does not detail which parts of C or Verilog are supported or which languages come next.