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 the code to verify, such as a C source tree or a SystemVerilog design, and any file of requirements. Send your code as it is, and Aristotle writes the proofs. Projects with only Lean files aren't supported. 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 tighten the requirements, fix what a counterexample found, or pick up from partial progress, and Aristotle keeps the context of earlier tasks. Continuing a finished project starts a new task, which uses credits.
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 (https://aristotle.harmonic.fun/mcp) 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())
Managing projects
Archive a project to remove it from your project list. In the web app, open the project's menu in Projects and choose Archive project. A project with a running task can't be archived until the task finishes or you cancel it. Archived projects move to the Archived projects section at the end of Projects and no longer appear in aristotle list. Shared links to an archived project keep working.
To restore a project, choose Unarchive project from its menu, or open it and send a prompt.
Delete a project to remove it for good. In the web app, open the project's menu in Projects, choose Delete project, and confirm. A deleted project can't be restored: its tasks and results go with it, and anyone who opens a shared link to it sees that it was deleted. A project with a running task can't be deleted until the task finishes or you cancel it. The credits its tasks used still appear in your organization's billing usage. With the CLI, run aristotle delete <project>. Through the MCP server, ask your assistant to delete a project. Both ask you to confirm first.
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.
