# Contracts

Check an action's input before it runs and its result after, with JEXL expressions.

`@Contract` declares **preconditions**, **postconditions** and **invariants**. The framework enforces them around every call to the action. A precondition rejects bad input, including arguments the model made up, before the method runs. A postcondition catches a wrong result or corrupted state after it runs.

A tool input schema, such as MCP's JSON Schema, checks only the shape of the arguments. A contract checks what they mean, and how the result relates to them.

## Declare a contract

```java
@ActionSpec(type = ActionType.LOCAL, description = "Withdraw from an account")
@Contract(
    preconditions  = {"amount > 0", "amount <= account.balance"},
    postconditions = {"account.balance == old(account.balance) - amount"},
    invariants     = {"account.balance >= 0"})
public Account withdraw(Account account, double amount) {
    account.balance -= amount;
    return account;
}
```

* A failed **precondition** throws before `withdraw` runs. The LLM gets a clear "precondition violated: amount > 0" and can retry with corrected arguments.
* The **postcondition** binds `old(account.balance)` to the pre-execution value, so it verifies the balance actually dropped by `amount`.
* The **invariant** is checked both before and after.

## Pair it with `@ActionSpec`

A contract runs only on an action. A method with `@Contract` but no `@ActionSpec` fails discovery with `IllegalStateException`:

```text
@Contract on com.example.Ledger.helper has no @ActionSpec; the clause is never evaluated. Annotate the method with @ActionSpec or remove @Contract.
```

## What each clause does

| Clause | When | On failure |
| --- | --- | --- |
| `preconditions` | before execution | always fails the call |
| `postconditions` | after execution | fails the call, or only logs when `strict = false` |
| `invariants` | before **and** after | always fails the call |

A failed clause reaches the caller as `ActionExecutionException` in category `VALIDATION`. Its cause is a `ContractViolationException`, which names the clause kind, the expression and its bindings.

Expressions are [JEXL](https://commons.apache.org/proper/commons-jexl/). Inside them you can reference the action's parameters by name, plus two special bindings in postconditions:

* **`result`**: the value the action returned (e.g. `result.success()`).
* **`old(expr)`**: the value `expr` had *before* execution, captured automatically (e.g. `old(account.balance)`). Use it to assert a delta.

### Flags

* `validate = false`: disables all enforcement for that action, and the contract becomes documentation only.
* `strict = false`: downgrades **postcondition** failures to a logged warning instead of throwing (preconditions and invariants always throw).
* `message = "…"`: overrides the default violation message.
* `inheritance`: declared, with `STRENGTHEN`, `LISKOV`, `REPLACE` and `NONE`, and a default of `STRENGTHEN`. It is not enforced. Each action is checked against its own `@Contract` only.

## Add a contract to a programmatic action

Actions added through `RoleBuilder.addAction(...)` have no annotated method, so they attach a contract with `ActionConfig.withContract(...)`. The `ContractSpec` builder is the programmatic equivalent of `@Contract`, enforced through the exact same code path:

<!-- java-contract: src/main/java/com/example/tnsai/docs/ContractSpecBuilderExample.java -->
```java
package com.example.tnsai.docs;

import com.tnsai.metadata.ActionConfig;
import com.tnsai.metadata.ActionHandler;
import com.tnsai.metadata.ContractSpec;
import com.tnsai.roles.Role;
import com.tnsai.roles.RoleBuilder;

public final class ContractSpecBuilderExample {
    private ContractSpecBuilderExample() {}

    public static Role banker(ActionHandler handler) {
        return RoleBuilder.create()
            .name("banker")
            .goal("Process withdrawals")
            .addAction(ActionConfig.local("withdraw", "Withdraw from an account", handler)
                .withContract(ContractSpec.builder()
                    .precondition("amount > 0")
                    .postcondition("result.success()")
                    .build()))
            .build();
    }
}
```

`ContractSpec.from(@Contract)` adapts an annotation into a spec, so the annotation and builder paths are indistinguishable at enforcement time.

## Catch typos at build time

`AgentBuilder.build()` parses every contract clause and reports a malformed expression as warning `AGENT-V013`. A typo then shows up at build time, not on the first call. If you build expressions at runtime, turn the check off with `.relaxValidation("AGENT-V013")` on the builder.

## Other ways to constrain an action

* **`@Contract`** (this page): JEXL preconditions, postconditions and invariants, with `old(...)` and `result`. Prefer it for new code.
* **`@State` invariants**, checked after the action when the method carries `@InvariantCheck`. See [Validation](../security/validation.md).
* **`@ActionSpec.precondition` and `postcondition`** are planning metadata. The framework does not check them when the action runs.
* **`ActionContract`**: an interface for contracts written in Java rather than as expression strings.

## Related

- [Actions](actions.md): where contract checks run in the action pipeline.
- [Validation](../security/validation.md): `@State` invariants.
- [Exceptions](exceptions.md): `ContractViolationException` and the other action errors.