Harmonic moves Aristotle from math proofs into C and chip verification

The story

Harmonic has expanded its Aristotle artificial-intelligence system from mathematical theorem proving into formal verification for C software and Verilog chip designs. Announced October 27 and available immediately under usage-based pricing, the service proposes properties from code and specifications, tries to prove or refute them, and reports the assumptions behind each result. The aim is to make an assurance technique long associated with specialist teams usable inside an ordinary engineering workflow.

Formal verification asks a different question from testing. A test observes selected executions; a proof can establish that a stated property holds for every input and state covered by a formal model. For C, Harmonic says Aristotle can address functional requirements and certain classes of undefined behavior. For Verilog, the language used to describe digital hardware, it targets control-path properties such as safety and liveness alongside mathematical properties of data paths.

The workflow still assigns a decisive role to people. Aristotle may infer candidate properties from code, documentation and prompts, but engineers review those properties before committing them to a repository. Approved claims can then run in continuous integration so later changes are checked against the same obligations. A result may be proved, refuted with a counterexample, or left open when the system cannot settle it. That last category is important: formal methods do not convert every difficult program into a guaranteed answer.

Harmonic’s largest disclosed hardware example comes from Tensordyne, an AI-chip company. In a case study published by Harmonic, Aristotle analyzed a partition described as 12.2 million gate equivalents, with 1.24 million flip-flops and 45 megabits of memory. Of 241 properties, the system proved 185 and refuted 56; the reported counterexamples exposed eight bugs, including one appearing 110,000 cycles after reset. Aristotle wrote 100 of the properties, while 141 already existed in the design. These are company and customer claims, not an independent benchmark.

A second case study concerns LibTomMath, the open-source multiple-precision arithmetic library used by projects including Tcl and Dropbear SSH. Harmonic says Aristotle identified three bugs and produced verified repairs, then optimized modular exponentiation by 31 to 38 percent in its own benchmarks while proving the revised implementation against the same specification. The result illustrates a useful combination of synthesis and proof, but neither Reuters nor an independent evaluation has yet reproduced the performance figures.

Reuters independently confirmed the C and Verilog launch and reported another example involving the U.S. DIII-D fusion facility. A program entry for an upcoming International Atomic Energy Agency workshop says Aristotle reconstructed a deployed plasma-control calculation from a research paper and a 254-word prompt, generated both C and Verilog versions, and proved them logically equivalent bit for bit. That workshop abstract supports the existence of the demonstration; it is not a peer-reviewed assessment of the product’s general reliability.

The technical trust comes from separating proof search from proof checking. Aristotle can use AI to draft reasoning, but Lean’s small kernel checks the resulting proof term before accepting it. Lean’s official documentation explains that errors in a tactic do not by themselves compromise a valid kernel check. Proof objects can also be exported and checked later or by a separate process, making the result more auditable than a model’s natural-language assertion that code is correct.

That architecture does not eliminate the specification problem. The kernel verifies that a proof establishes the formal statement it was given; it does not know whether the statement accurately expresses a safety requirement. A model of C may omit behavior outside its stated assumptions. A verified register-transfer design can still encounter faults in synthesis tools, timing, analog components or fabricated silicon. Libraries and axioms in the trusted base also matter. ‘Proved correct’ therefore needs an attached object: correct with respect to which properties, semantics and environment.

INNOVOX analysis: the important product shift is automated property creation. Proof assistants have long offered strong guarantees once experts formalize the right claims, but writing those claims and completing the proofs is expensive. An agent that can read specifications, flag contradictions and generate checkable obligations could broaden adoption. The risk is assurance theatre: a large count of proved properties may look comprehensive even when a crucial requirement was never formalized. Coverage must be explained in engineering terms, not only proof totals.

What to watch is independent evidence. Harmonic can strengthen the case by publishing representative properties, counterexamples, proof objects and the exact semantic models used for C and Verilog, while preserving customer confidentiality. Outside teams should test the system on unfamiliar repositories and measure setup effort, false confidence, unresolved goals and maintenance cost—not just bugs found. Aristotle has shown that AI can help make formal verification more accessible; the next test is whether the resulting guarantees remain meaningful after the demonstration ends and the code keeps changing.

INNOVOX analysis

Aristotle’s consequential move is not replacing tests with proofs. It is lowering the labor needed to write properties and construct proofs, which shifts the engineering bottleneck toward specification review. If teams do not scrutinize what is being proved, stronger automation can produce precise assurance about the wrong requirement.

What to watch

Watch for public proof artifacts, independently reproduced results on uncurated code, disclosure of the C and Verilog semantics in the trusted base, and evidence that ordinary engineering teams can maintain verified properties after the initial demonstration.