# aura prove *Mathematically verify that a behavioral goal is implemented by the current code.* ## Synopsis ```bash aura prove "" [--explain] [--strict] [--format=text|json] [--at ] ``` ## Description `aura prove` takes a plain-English goal and answers the question *"is this actually implemented?"* It does so by resolving the goal into a set of required logic nodes and required edges between them, then checking the current semantic graph to see whether those nodes exist and whether they are wired together. The output is either PROVED, PARTIAL (with a list of missing or unwired pieces), or UNPROVED. Unlike a test, `prove` does not execute anything. It reasons over the static graph: which functions exist, which call which, what types flow where, which error paths are handled. This is valuable because it tells you about the *shape* of the implementation — whether the pieces are present and connected — without requiring the code to be runnable, without test fixtures, and without side effects. A passing `aura prove` does not guarantee correctness; it guarantees the code's skeleton is consistent with the goal. Goals are written in a casual imperative style: `"User can authenticate via OAuth"`, `"Webhook retries use exponential backoff"`, `"Refunds cannot be issued after 180 days"`. Aura uses the description, the logic graph, and optionally an LLM resolver to map each goal into verifiable predicates. ## How a goal is resolved to logic nodes Resolution happens in three stages. First, the goal is **parsed into claims**. `"User can authenticate via OAuth"` becomes claims like *there exists an entry point accepting OAuth credentials*, *there exists a token verification path*, *the success path creates a session*, *the failure path returns an error*. Second, each claim is **grounded** to the logic graph. Aura searches for nodes whose names, signatures, type flows, and call relationships satisfy the claim. A claim about "OAuth credentials" is satisfied by a function whose parameter type mentions an OAuth token type and whose body calls into an OAuth verification module, or whose intent history mentions OAuth. If multiple candidates match, the best-scoring one is picked and shown. Third, the **wiring is checked**. Each grounded node is verified to be reachable from an entry point (HTTP handler, CLI command, scheduled job, etc.), and the required edges between claims are verified to exist in the call graph. Missing edges are reported as *gaps*. Goals can also be registered as named tests in `aura.toml` so they run as part of `aura pr-review`; this turns a one-off `prove` invocation into a permanent acceptance criterion. ## Flags | Flag | Description | | --- | --- | | `""` | Natural-language description. Quote it. | | `--explain` | Show the intermediate claims, chosen groundings, and edges checked. | | `--strict` | Exit non-zero on PARTIAL as well as UNPROVED. | | `--format=text` | Default. Human-readable with colored markers. | | `--format=json` | Structured result, suitable for CI. | | `--at ` | Prove the goal against a specific commit, save id, or branch tip instead of the working tree. | | `--save` | Persist the goal into `aura.toml` so it is re-checked on every PR. | ## Examples ### 1. A passing proof ```bash aura prove "User can authenticate via OAuth" ``` ```text PROVED — "User can authenticate via OAuth" Claims satisfied (4/4): ok entry point accepts OAuth token -> fn api::auth::oauth_login (src/api/auth.rs) ok token is verified against provider -> fn auth::oauth::verify_token ok success creates a session -> fn session::SessionStore::create ok failure returns a typed error -> enum auth::Error::InvalidToken ``` Each claim is shown with the node that satisfied it. You can follow the call chain with `aura trace` or `aura diff`. ### 2. A partial proof ```bash aura prove "Webhook retries use exponential backoff" ``` ```text PARTIAL — "Webhook retries use exponential backoff" Claims satisfied (2/3): ok there is a retry loop on webhook delivery -> fn webhooks::dispatcher::send_with_retry ok the loop increases the delay between attempts -> fn webhooks::dispatcher::compute_next_delay missing the backoff factor is ≥ 2 (or configurable) heuristic: compute_next_delay multiplies by 1.5; goal implies ≥ 2 suggestion: raise factor, or parameterize the factor and expose in config ``` The missing claim is explained, not just flagged. In strict mode this would exit `2`. ### 3. Explain the reasoning ```bash aura prove "Refunds cannot be issued after 180 days" --explain ``` Prints the claim tree, the candidate groundings that were considered and rejected (with scores), the chosen groundings, and the edges in the call graph that were traversed. Useful when `prove` gives a surprising verdict. ### 4. CI-friendly JSON ```bash aura prove "Account deletion is soft-delete" --format=json --strict ``` ```text {"goal":"Account deletion is soft-delete","verdict":"PROVED","claims":[{"text":"deletion sets a deleted_at timestamp","status":"ok","node":"fn Account::soft_delete"},{"text":"queries exclude soft-deleted rows by default","status":"ok","node":"fn AccountRepo::active_query"}],"elapsed_ms":312} ``` ### 5. Prove against an old commit ```bash aura prove "Refunds cannot be issued after 180 days" --at v0.11.0 ``` Re-runs the proof against the `v0.11.0` tag's semantic graph. Useful for bisecting when a behavioral invariant was lost. ## Good goals vs bad goals - **Good:** *"Every HTTP handler rate-limits per user."* Concrete, checkable against the call graph. - **Good:** *"Money values never flow from user input directly into a DB write without passing through validation."* Checkable via type-flow. - **Poor:** *"The code is fast."* Not a static-graph property. - **Poor:** *"Users are happy."* Not a code property at all. Prefer goals that name a behavior an auditor or new engineer would want to confirm by reading code. Avoid goals that require running the code to answer. ## Exit Codes | Code | Meaning | | --- | --- | | `0` | PROVED. Also PARTIAL when `--strict` is off. | | `2` | UNPROVED, or PARTIAL when `--strict` is on. | | `3` | Goal could not be parsed or grounded at all. | | `4` | `--at ` could not be resolved. | ## Writing goals that ground well A goal grounds well when it names observable behavior in the system's own vocabulary. Use the terms the codebase already uses — if the code calls the thing a `Session`, write *"a Session is created on login"*, not *"a user's auth context is stored"*. The grounding engine scores candidates by name similarity, so matching vocabulary matters. A goal grounds poorly when it is written entirely in abstractions the code has no names for. *"The system maintains referential integrity"* is abstract; *"every Order has a non-null customer_id that points to an existing Customer"* is concrete. Prefer the concrete phrasing. When a goal does not ground, `--explain` will show you what it was looking for and what it found. Edit the goal to match the vocabulary the explanation uses, or add the missing nodes to the code. ## Caching and reproducibility Each proof run memoizes its grounding decisions under `.aura/proofs/cache/`. Subsequent runs on the same graph reuse the grounding and only re-check the wiring, which is fast. When the LLM resolver is enabled, its outputs are also cached; a cache hit is deterministic, a cache miss consults the resolver. Cache entries are invalidated when the affected nodes change. This means `aura prove` in CI is fast after the first run and deterministic. Two CI runs of the same commit produce identical verdicts. ## Disabling the LLM resolver If your environment prohibits LLM calls, set `proofs.resolver = "structural"` in `aura.toml`. The structural resolver uses only name matching and call-graph heuristics, which is strictly weaker but fully local. Goals that would need the LLM to ground will return `UNRESOLVABLE` rather than making a network call. ## Saved proofs as acceptance criteria Running `aura prove "" --save` registers the goal in `aura.toml` under `[[proofs]]`: ```text [[proofs]] id = "auth_oauth" goal = "User can authenticate via OAuth" added_by = "ashiq@naridon.io" added_at = "2026-04-10T11:00:00Z" strict = true ``` Saved proofs are re-run on every `aura pr-review` and on every CI invocation of `aura prove --all`. A previously-proved goal that becomes UNPROVED is a regression; the PR that caused it is flagged. This turns `aura prove` into a running contract on the codebase: once a behavioral property is proved, you cannot silently break it. ## Limits of static proof `aura prove` is a static analysis. It does not execute the code and therefore does not know about runtime-only properties. It cannot tell you whether a regex is correct, whether a SQL query returns what you expect, whether a distributed protocol is live, or whether a cryptographic construction is secure. It can tell you whether the call graph matches the shape a correct implementation would have. In practice the most valuable goals are **structural invariants** — *every HTTP handler passes through the auth middleware*, *no code path writes to the billing DB without acquiring a lock*, *all external HTTP calls go through the rate-limited client*. These are properties that reviewers care about and that are easy to silently violate during refactors. Static proof catches them. ## Integration with LLM agents When an AI agent is making changes, the agent is expected to run `aura prove` before calling `aura save`. A PARTIAL or UNPROVED result on a previously-proved goal is a clear signal to the agent that the change is incomplete. This is one of the primary reasons proofs exist: agents are good at plausible-looking patches and bad at closing the loop on behavioral invariants. ## See Also - [aura diff](/aura-diff) — inspect the nodes a proof depends on - [aura trace](/aura-trace) — see how a proof's grounded nodes evolved - [aura pr-review](/aura-status) — runs saved proofs automatically - [aura save](/aura-save) — associates intent text that helps future proofs ground faster