Developer documentation

ActionProof

Last reviewed 31 August 2026

ActionProof

ActionProof verifies a *plan* -- an ordered list of tool calls the agent intends

to make -- against your declared constraints, using an SMT solver. It answers

"can this sequence violate a constraint?" before any of it runs.

Enabling it

verification:
  actionproof: true
  profile: billing-constraints

Both lines matter. With actionproof: true and no profile, there are no

constraints to prove against, so verification reports not_configured -- which

is not a denial, and is not verification either. cain doctor warns about

exactly this state, because it is the one most easily mistaken for protection.

Submitting a plan

cain verify --plan '[{"tool":"refund","args":{"amount":500}},
                     {"tool":"refund","args":{"amount":500}}]'

decision = cain.verify(
    action="execute_plan",
    plan=[{"tool": "refund", "args": {"amount": 500}},
          {"tool": "refund", "args": {"amount": 500}}],
)

Without a plan, the verification stage reports skipped -- there is nothing to

verify. A single call is not a plan.

What it does and does not prove

It discharges real SMT queries about specific, bounded properties you have

declared. That is genuinely stronger than a heuristic.

It is not a proof that your agent is correct, that the platform is correct,

or that unlisted constraints hold. We do not describe it as one, and the

gaps page says so publicly.

Reading the result

cain explain <decision-id>

The actionproof stage reports one of:

unavailable becomes UNKNOWN at the client under strict mode, and UNKNOWN is

not permission.