Documentation
Overview
Aristotle is a verified reasoning agent by Harmonic. Give it existing code and it proves the properties you specify, or finds bugs and suggests verified fixes. Every proof is machine-checked. C refutations require a concrete counterexample. Hardware refutations are supported by a concrete counterexample, a formal proof of the negation, or both.
You describe the properties in plain English. Aristotle works directly in your C and SystemVerilog files and tells you exactly what it proved, what it assumed, and what it could not prove and why.
What Aristotle can do
Verify existing code. Submit C code or a SystemVerilog design and describe the properties you want checked. Aristotle can prove, for example, freedom from undefined behavior and functional properties in C, and functional, safety, and liveness properties in supported SystemVerilog designs. Proofs depend on stated preconditions and assumptions.
Find counterexamples. When a property is false, Aristotle does not stop at a failed proof. For C you get a small program that reproduces the failure. For SystemVerilog, a concrete counterexample comes with a testbench or harness and a VCD waveform.
Fix with proof. When a property is refuted, Aristotle can suggest and implement fixes and verify the revised code against the requirements you stated.
Specify in English. No annotation language to learn. Write the properties you care about in the prompt or in a text file alongside your sources, and Aristotle reports exactly what it proved and what it had to assume.
What "verified" means
A proof covers the properties you stated, under the assumptions listed in the summary. When Aristotle fixes code, the revised code is verified against the requirements you stated. If a behavior matters, state it as a requirement.
How it works
Every submission is a project: a prompt plus any files it needs, such as a C source tree, a SystemVerilog design, or a file of requirements. Aristotle runs a task against the project and returns a written summary of what it proved, what it assumed, what it changed, and any counterexamples it found, along with the files it produced or edited.
Projects are conversations. You can continue one to ask about the result, tighten the requirements, or pick up from partial progress, and Aristotle keeps the context of earlier tasks.
Ways to use Aristotle
Web app. Sign in at aristotle.harmonic.fun, type a prompt, attach files or a folder, and follow the run from your browser.
MCP. Add Aristotle's MCP server to your AI assistant, sign in, and ask it to verify your code: it uploads the project, starts the run, follows it and reads the results.
CLI. Run aristotle from your terminal to submit projects, follow progress, download results, and manage your work.
aristotle submit "Prove that every function in this project is memory safe" --project-dir ./ring-buffer --wait
Continue in the same project to refine the result or resume from partial progress:
aristotle continue <project-id> "rb_push drops values when the buffer is full. Fix it and prove no value is lost." --wait
Python SDK. Use the aristotlelib package for automation and integration.
import asyncio
from aristotlelib import Project
async def main():
project = await Project.create_from_directory(
prompt="Prove that every function in this project is memory safe",
project_dir="./ring-buffer",
)
tasks, _ = await project.get_tasks(limit=1)
await tasks[0].wait_for_completion()
await project.get_files(destination="output.tar.gz")
asyncio.run(main())
Next steps
To get started, see MCP & CLI.
For a full walkthrough of each language, including example projects and current limitations, see the software verification and hardware verification guides.