Aristotle Brings Formal Verification to C and Verilog, Finding Bugs 110,000 Cycles Deep in Tensordyne's Hardest Block
Synopsis
Harmonic has extended Aristotle, previously applied to research mathematics, to formal verification of software and hardware, starting with C and Verilog. Unlike code review and testing, which examine only a portion of possible behaviors, it uses machine-checked proofs to determine whether specified properties hold across all possible inputs within a defined system, proposing properties from code and reporting which were proved and what assumptions each proof rests on. In the block Tensordyne's team considered hardest to verify, it found bugs up to 110,000 cycles deep; on LibTomMath it fixed three bugs and made modular exponentiation 31–38% faster in Harmonic's benchmarks, with the faster code proved against the same spec.
Interpretation
Formal verification is being offered to ordinary engineering teams rather than only specialists, starting with C and Verilog. Formal verification has always been slow and costly, and mostly limited to specialists. Harmonic applies the same technology it proved in research mathematics, AI reasoning grounded in machine-checked proofs, to software and hardware.
The tool proposes properties from existing code, reports which it proved, which it did not, and the assumptions each proof rests on, and engineers review the properties, commit them to the repository, and run it in CI on every commit. Code review and testing examine only a portion of possible behaviors, whereas formal verification mathematically proves specified properties across all possible inputs within a defined system. For C it verifies functional correctness and the absence of certain classes of undefined behavior; for Verilog it covers control-path liveness and safety plus mathematical data-path properties.
On real code, Aristotle found bugs up to 110,000 cycles deep in the block the Tensordyne team considered hardest to verify. That depth goes far beyond what ordinary testing reaches. The result comes from Tensordyne's actual block rather than a synthetic example.
On LibTomMath, the big-number library behind Tcl and Dropbear SSH, Aristotle fixed three bugs and made modular exponentiation 31–38% faster in Harmonic's benchmarks. The faster code was proved against the same spec, so the speedup and the correctness proof hold together. The comparison is a benchmark Harmonic reports for modular exponentiation in LibTomMath.
Perspective
The demonstrated scope is two languages: for C, verification of functional correctness and the absence of certain classes of undefined behavior; for Verilog, control-path liveness and safety plus mathematical data-path properties. The tool is available today with self-serve, consumption-based pricing and enterprise plans.
Proof results depend on the proposed properties and on the assumptions each proof rests on, so engineers must review the properties; the performance figures come from Harmonic's own benchmarks, and the bug depth and speedup apply to the specific codebases named.