Harmonic, the AI startup co-founded by Robinhood Chairman and CEO Vlad Tenev, has expanded Aristotle to check C software and Verilog hardware against specified requirements, giving engineering teams a formal way to test designs.
Harmonic describes the system as using mathematical proofs to assess requirements. Its C checks include functional correctness and some forms of undefined behavior; for Verilog, the company cites control-path and data-path properties. Aristotle analyzes code to suggest properties for testing, then reports which it proved and which it could not prove, along with the assumptions behind each result. A proof concerns a specified property across every possible input in the defined system.
At the DIII-D National Fusion Facility, authors affiliated with General Atomics say Aristotle examined Verilog already used in a Thomson-scattering diagnostic system and identified multiple rare errors. They report that finding the errors manually could have taken days.
The authors also describe a separate conversion exercise. Starting with a research paper and a 254-word prompt, Aristotle recreated C code for attachment-fraction calculations and generated a Verilog counterpart for FPGA acceleration. The authors say it proved the two versions logically equivalent bit for bit on the first attempt; that exercise took four hours.
Harmonic made Aristotle available Oct. 27 through a self-service model with consumption-based pricing. The company did not disclose a price. It says the expansion responds to software being produced faster than teams can review it, and describes formal verification as slow, costly and limited to specialists. Harmonic co-founder and CEO Tudor Achim said mathematical verification is “a new way to identify defects and vulnerabilities.”
Harmonic announced a $120 million Series C on Nov. 25, 2025, and said the funding round valued the company at $1.45 billion.
The DIII-D findings are presented in an abstract for the International Atomic Energy Agency’s AI for Fusion workshop, scheduled for Nov. 9-11. C. Mitchell Clark of General Atomics is listed to present on Nov. 9 at 6:30 a.m. ET (11:30 UTC).
