ActionProof

All docs

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:

verdict	meaning
allow	the solver found no violation of your constraints
deny	the solver found a violation -- and can usually name the step
not_configured	no profile: nothing to prove against
skipped	no plan submitted
unavailable	the service could not be reached

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