Harmonic launched Aristotle for software and hardware verification. The expansion starts with C and Verilog. Aristotle is available to engineering teams today.
What Aristotle does
Aristotle uses formal verification grounded in machine-checked proofs. It proposes properties from existing code and reports which ones it proved. Teams can commit those properties and run Aristotle in CI on every commit.
Early results
At Tensordyne, Aristotle found bugs up to 110,000 cycles deep. The bugs were in the block the team considered hardest to verify. On LibTomMath, it fixed three bugs and made modular exponentiation 31% to 38% faster against the same spec.
What it supports
For C, the tool verifies functional correctness and the absence of certain classes of undefined behavior. For Verilog, it covers control-path properties such as liveness and safety. It also covers mathematical data-path properties.
Teams can sign up for self-serve, consumption-based pricing. Enterprise plans include volume pricing and dedicated support. They also offer on-prem or private-cloud deployment options.