Common questions

Can Aristotle still prove mathematics or work on a Lean project?

Aristotle verifies C and Verilog. Projects with only Lean files aren't supported, and a project like that finishes with a notice saying so. Your existing projects stay in your project list, and the files already delivered in them stay downloadable. Lean support will return in the coming months.

Which languages can Aristotle verify?

Aristotle verifies C and Verilog on every account. It works out the languages from your prompt and from the files you upload, so there is nothing to declare. A project with no source in a supported language, such as a C# codebase or a paper in LaTeX or PDF, finishes with a summary saying that no supported source was uploaded, and nothing is verified. More languages are coming soon.

Do I get the proofs back, or just a pass or fail?

Every task returns a written summary and the project's Properties table, where each property carries its status and its evidence. You also get:

• Your sources, with any edits Aristotle made at your request.
• For a SystemVerilog design, the formal statements of the properties and the design's public interface files.
• For each concrete counterexample, a reproducer you can run yourself: a C program, or a SystemVerilog testbench or harness with a VCD waveform.

See Hardware verification and Software verification.

What happens when my organization runs out of credits?

A running task stops with the status Out of Credits, and no new task starts until the balance is topped up. Your projects, their files, and their results stay in your account and stay readable. When an organization admin adds credits, tell Aristotle to continue and it picks up from where the task stopped. Admins see the balance, buy credits, and review usage by project under Settings › Billing.

Does a project use credits even if it ends without changing anything?

Yes. A project draws credits for the work it does, whatever its outcome, including a follow-up task that ends without editing a file. A follow-up builds on the work of earlier tasks in the project, so it usually uses fewer credits than starting a new project. See Overview.

Can I include a paper or specification document, such as LaTeX, in my project?

A project needs source in a language Aristotle verifies: C or Verilog. Write the properties you want checked in the prompt, or in any text or Markdown file you include with the sources and reference from the prompt. Other documents can go up alongside them as background, such as API docs and conceptual docs for a dependency. See C verification and Hardware verification.

Can I delete a project?

Yes. In Projects, open the project's menu, choose Delete project, and confirm. A deleted project can't be restored, and anyone who opens a shared link to it sees that it was deleted. If a task is still running, wait for it to finish or cancel it first. The credits the project 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 the project. If you only want it out of your list, archive it instead, and you can unarchive it later. See Managing projects.