Documentation
Tracking properties
When Aristotle verifies code, a project turns into a list of properties: the statements Aristotle proves or refutes about that code, each one with its own outcome. aristotle submit prints a link to the project, and the properties table there is where the work shows up while it happens.
The project view
A project page has three panes (Properties, Code, and Agent) that you can open, close, reorder, and resize. Properties and Agent are open to begin with. The pane in front is in the URL, so a link opens on what you were looking at:
https://aristotle.harmonic.fun/projects/<project-id>?view=props
Properties and definitions
The table has two tabs. Properties are the statements Aristotle proves; Definitions are the objects those statements are about. Only properties carry a status, because only they have something to prove.
Each row shows the name, a one-line description, and when it last changed. Open a row for the full description, any refutation evidence, and related files to download under Artifacts, such as a counterexample's trace. Open in code jumps to the property definition in the code pane when one is available.
Status
In progress. The property has no verdict yet.
Proved. Aristotle proved the property, under the assumptions the summary lists.
Refuted. The property is false. Its evidence is a concrete counterexample, a formal proof of its negation, or both.
Unknown. This page doesn't know the status Aristotle sent, as can happen just after an update. Reload the page.
Unresolved. The property isn't verified. The run that worked on it ran out of time, hit a system error, was canceled, or ended with errors before verifying it, or its proof failed the project's final check. Open the row for the reason.
A run that stops or runs out of budget can leave some properties unresolved. It does not invalidate results already established for unchanged properties.
A formal proof of negation and a counterexample are both evidence for a refutation. They usually mean the specification says something other than what you meant, or the code does something you did not intend. The proof of the negation, or the counterexample itself, shows where.
The counts above the table say how many properties are in each state. Click one to show only those, and click it again to go back to all of them.
Sorting and grouping
The filter menu to the right of the counts holds two settings:
- Group by:
None, orFileto fold the table into one collapsible group per file that holds the results. - Sort by:
Updated(the default),File order,Created,Name, orStatus.
Status, sort, and grouping all live in the URL alongside the pane, so what you are looking at is what you send to a colleague:
https://aristotle.harmonic.fun/projects/<project-id>?view=props&status=refuted&sort=name&group=file
While a run is going
Properties appear as Aristotle extracts them, and their statuses change as it works, so an empty table early in a run means it is still reading your code. The Agent pane shows what it is doing in the meantime.
From the terminal
The same table is one command away:
aristotle properties <project-id> --status REFUTED --sort name
It lists properties most recently updated first. --status narrows it as clicking a count does, --sort (updated, created, or name) reorders it as Sort by does, --kind definition switches to the Definitions tab, and --json prints the full records. The terminal labels refutations REFUTED, and its EVIDENCE column distinguishes a counterexample, a formal proof of the negation, or both. --status REFUTED lists all refutations. The CLI uses (unchecked) for results from runs that ended early. aristotle property <project-id> <name> shows one in full: its statement, status, and where it came from.
aristotle show <project-id> prints the counts and, at a terminal, live-tails a run that is still going. aristotle submit --wait stays attached from the start.