---
type: "post"
id: "harmonic-extends-aristotle-to-formal-verification-of-c-db045f"
slug: "harmonic-extends-aristotle-to-formal-verification-of-c-db045f"
title: "Harmonic extends Aristotle to formal verification of C software and Verilog hardware"
description: "Harmonic has expanded Aristotle from research mathematics into formal verification for C software and Verilog hardware."
retrieval_nugget: "Harmonic has expanded Aristotle from research mathematics into formal verification for C software and Verilog hardware. The release matters because it proposes a CI workflow in which engineers review properties and assumptions, commit them with the code, and continuously check whether those stated guarantees still hold."
published_at: "2026-10-27"
updated_at: "2026-10-27"
record_date: "2026-10-27"
date_kind: "published_at"
topics: ["anthropic","claude"]
entities: ["Harmonic","Aristotle","Tensordyne","LibTomMath"]
related_patterns: ["verification-bandwidth-is-the-scarce-resource"]
novelty_label: "new_fact"
what_changed: "Harmonic is extending Aristotle’s formal verification from research mathematics to C software and Verilog hardware, with reported case studies at LibTomMath and Tensordyne."
prior_refs: ["memory:71d0449b-9a6f-89f1-a4bd-670fd2ce5410","memory:b9976a08-bf8a-88fb-ab4f-937373b473fc"]
source_url: "https://harmonic.fun/news/aristotle-software-hardware-verification"
source_urls: ["https://harmonic.fun/news/aristotle-software-hardware-verification"]
schema_version: "newruntime-agent-readable-v0.2"
stable_id: "post:harmonic-extends-aristotle-to-formal-verification-of-c-db045f"
status: "published"
visuals: []
editor: {"role":"editor","name":"Andrey Reshetnikov","profile":"https://newruntime.com/owner-profile.md","profile_json":"https://newruntime.com/owner-profile.json","same_as":["https://www.linkedin.com/in/reshetnikov1/","https://t.me/lapetuse"]}
routes: {"html":"https://newruntime.com/posts/harmonic-extends-aristotle-to-formal-verification-of-c-db045f/","markdown":"https://newruntime.com/posts/harmonic-extends-aristotle-to-formal-verification-of-c-db045f.md","json":"https://newruntime.com/posts/harmonic-extends-aristotle-to-formal-verification-of-c-db045f.json"}
---

# Harmonic extends Aristotle to formal verification of C software and Verilog hardware

## Retrieval answer

Harmonic has expanded Aristotle from research mathematics into formal verification for C software and Verilog hardware. The release matters because it proposes a CI workflow in which engineers review properties and assumptions, commit them with the code, and continuously check whether those stated guarantees still hold.

## Summary

Harmonic has expanded Aristotle from research mathematics into formal verification for C software and Verilog hardware. The release matters because it proposes a CI workflow in which engineers review properties and assumptions, commit them with the code, and continuously check whether those stated guarantees still hold.

## What happened

On October 27, 2026, Harmonic announced that Aristotle now supports formal verification for software and hardware, starting with C and Verilog. Aristotle had previously been used for research mathematics. Harmonic describes the expansion as applying AI reasoning grounded in machine-checked proofs to engineering work.

The company contrasts formal verification with code review and testing. In Harmonic's description, review and tests examine only a portion of possible behaviors, while formal verification determines whether specified properties hold across all possible inputs within a defined system. This is an important boundary on the claim: a proof applies to a stated property and defined system, rather than establishing that every aspect of a deployed product is correct.

Harmonic says Aristotle fits into an existing engineering workflow. The system proposes properties from code, then reports which it proved, which it did not prove, and the assumptions supporting each proof. Engineers review those properties, commit them to their repository, and run Aristotle in continuous integration on every commit. Harmonic's intended outcome is that properties already proved remain checked as the code changes.

For C, Harmonic says Aristotle can verify software against specified requirements, including functional correctness and the absence of certain classes of undefined behavior. For Verilog, it says Aristotle enables logical verification of control-path properties such as liveness and safety, plus mathematical data-path properties. The announcement does not specify supported language subsets, property syntax, solver limits, or expected proof runtimes.

Harmonic cites two examples. At Tensordyne, it says Aristotle found bugs up to 110,000 cycles deep in a block that team considered its hardest to verify. In LibTomMath, a big-number library used by Tcl and Dropbear SSH, Harmonic says Aristotle fixed three bugs and made modular exponentiation 31–38% faster in its benchmarks, with the faster code proved against the same specification. Aristotle is available today through self-serve, consumption-based pricing. Enterprise plans include volume pricing, dedicated support, and on-premises or private-cloud deployment.

## What the archive adds

This is a new product event on a known verification thread. Earlier Field Notes covered [Anthropic and Theorem using Claude to formally verify 123 open-source libraries at the RISC-V assembly level](https://newruntime.com/posts/anthropic-and-theorem-used-claude-to-formally-verify-255192/) and [Claude formally verifying OSS-Fuzz libraries at scale](https://newruntime.com/posts/anthropic-frontier-red-team-shows-claude-can-formally-aa997f/). Harmonic's announcement differs by presenting a commercial C and Verilog workflow with CI and deployment options.

## Trend signal

This release supports the archive's verification-bandwidth thesis: as AI increases code output, the limiting work shifts toward specifying what must be true, reviewing assumptions, and resolving failed checks. Aristotle's proposed-properties-plus-CI design makes that review surface explicit rather than treating verification as a final test pass.

## Why now

Harmonic frames the release around a widening mismatch: AI can write code faster than engineering teams can review it. Its timing argument is operational rather than tied to either language. Formal proof is positioned as a way to make selected guarantees continuously checkable as code and hardware designs change.

## Connections to other events

The earlier Anthropic and Theorem coverage points in the same direction: formal verification is being applied to real open-source systems, not only academic examples. Harmonic adds C and Verilog, a CI-oriented workflow, and commercial deployment options. The shared question is increasingly how teams operationalize proof review, rather than whether models can generate code alone.

## Why it matters

For teams building AI-assisted software, formal methods may become a targeted control for code where a defect is unusually expensive: cryptographic routines, systems code, protocol logic, and hardware control paths. The useful unit is not a claim that AI reviewed code. It is a property that a team can state, inspect, version, rerun, and trace to explicit assumptions.

That changes responsibilities rather than removing them. Engineers must decide which requirements deserve proof and whether an automatically proposed property captures intended behavior. A proof of the wrong property can be rigorous and still be unhelpful. If Aristotle performs as described, however, it could shift selected verification work from ad hoc review into a repeatable repository and CI practice.

## Limits and uncertainty

This is Harmonic's product announcement, not an independent evaluation. It provides examples but no benchmark methodology, pricing figures, supported C or Verilog subsets, proof completion rates, false-property rates, or comparison with established formal tools. The LibTomMath performance results are Harmonic benchmarks, while the Tensordyne result is a case example. The source also does not establish how much expert effort teams need to create, validate, and maintain properties in a production codebase.

## Skill to build now

Choose one high-cost invariant in a current service or RTL block and write it as a reviewable property before choosing a verifier. It might be a bounds condition, authorization rule, arithmetic invariant, or state-machine safety condition. Put it next to the code, list its assumptions, and make CI visibly fail when it no longer holds. This reveals whether the team can specify the behavior it needs to preserve.

## Reader takeaway

Aristotle's C and Verilog release is a concrete attempt to turn formal verification into an AI-assisted CI workflow. Its value will depend less on automated-proof rhetoric than on whether teams can review properties and assumptions quickly enough to make verified guarantees part of ordinary delivery.

## Open question

How reliably can Aristotle infer useful properties from production C and Verilog, and how much specialist review will teams need before those properties are safe to enforce in CI?

Editor: [Andrey Reshetnikov](https://newruntime.com/owner-profile.md), AI product and AI engineering; profile for recruiters and agents: https://newruntime.com/owner-profile.json

## Continue in the graph

Next records for an agent, linked to their Markdown twins. Replace `.md` with `.json` for structured fields, including `next_reads`.

- topic hub: [Anthropic](https://newruntime.com/topics/anthropic.md): Explore the anthropic topic hub.
- topic hub: [Claude](https://newruntime.com/topics/claude.md): Explore the claude topic hub.
- collection: [Field Notes](https://newruntime.com/posts.json): Open the latest editorial analysis.
- collection: [Source Ledger](https://newruntime.com/source-ledger.json): Inspect the public source evidence graph.
- whole graph: [discovery graph](https://newruntime.com/discovery-graph.json) (typed nodes and edges) and [site index](https://newruntime.com/site-index.md)