Writing Effective Policies

Your policy is the foundation of everything ICME does. When you submit a policy to /v1/makeRules, it is formalized into a mathematically precise model expressed in SMT-LIB2. The compiler checks the resulting rules for internal consistency. What reaches the solver is an exact, provable representation of what you wrote, which means the quality of your guardrail is directly determined by the quality of your policy text.

---

Limits

Resource	Limit
Max rules per policy	50
Max policy length	5,000 characters
Max action length	2,000 characters

---

How the compiler reads your text

The translator maps each sentence to a (premise) → (consequence) relationship and identifies variables by recognizing the same concept expressed consistently across rules.

Clarity beats cleverness. Write policies the way you would explain rules to a new employee, not the way you would write a legal contract. Short, declarative if-then sentences formalize more reliably than long, nested clauses.

Ambiguity becomes ambiguity. Vague terms like "large," "generally," or "should check" do not compile into precise constraints. If a rule has an exception, write the exception. If a limit applies under certain conditions, write the conditions. Ambiguous rules produce SATISFIABLE results rather than clean SAT or UNSAT.

---

Policy structure

Write your policy as a numbered list of plain English if-then rules. Each rule should express exactly one condition and exactly one outcome.

# Good
1. If the transfer amount exceeds 1000 USDC, then the transfer is not permitted.
2. If the recipient address is not in the approved registry, then the transfer is not permitted.
3. If more than 3 transfers have occurred within the last 60 seconds, then the transfer is not permitted.

# Harder to formalize
1. Large transfers to unknown wallets are generally not permitted unless
   pre-approved, and the agent should also be careful about frequency.

The second version will compile, but the rules it produces will be less precise. "Large" is undefined. "Generally" introduces ambiguity. "Should also be careful" is not a constraint.

---

One outcome per statement

The solver maps each sentence to a single (premise) → (consequence) relationship. If a sentence produces two consequences, even joined by "and," the translator may drop one silently.

# Wrong
If the transfer amount exceeds 100, then the transfer is not permitted and the action must be rejected.

# Right
If the transfer amount exceeds 100, then the transfer is not permitted.
If the transfer amount exceeds 100, then the action must be rejected.

Repeat the condition. Write two rules. The redundancy is intentional — it ensures both consequences are captured as separate enforceable constraints.

---

Consistent terminology is enforcement

If you use different phrases for the same concept — "recipient wallet," "destination address," "target account" — the translator may create three separate variables that never connect. A rule about recipient wallet will not fire when the action describes a destination address.

Pick one noun phrase per concept and use it exactly throughout the entire policy.

# Poor — three variables that may never connect
1. Transfers to unapproved wallets are not permitted.
2. Payments to unknown destination addresses must be blocked.
3. The target account must appear in the verified list.

# Good — same variable, three edge cases, three rules
1. If the recipient address is not in the approved registry, then the transfer is not permitted.
2. If the recipient address is unknown, then the transfer is not permitted.
3. If the recipient address is unresolved, then the transfer is not permitted.

---

Common mistakes

Relative terms without definitions

# Wrong — "large" is meaningless to formal logic
Large transactions require approval.

# Right
If the transaction amount exceeds 5000, then approval is required.

Bundling multiple constraints

# Wrong — four constraints, two consequences, one sentence
Large transfers to new wallets outside business hours require approval and must be logged.

# Right
If the transfer amount exceeds 5000, then approval is required.
If the recipient wallet was created within the last 30 days, then approval is required.
If the transfer occurs outside business hours, then approval is required.
If a transfer occurs, then a transfer receipt must be generated.

Process language instead of constraint language

# Wrong — describes a step, not a constraint
The agent should check the whitelist before making transfers.

# Right
Transfers are only permitted to wallets on the approved whitelist.

Conflicting rules

# Wrong — produces IMPOSSIBLE for any external, unverified wallet
1. All transfers to external wallets are permitted.
2. Transfers to unverified wallets are not permitted.

# Right
1. Transfers to wallets on the verified list are permitted.
2. Transfers to all other wallets are not permitted.

Implicit exceptions

# Wrong — blocks the emergency fund too
No transfers over 1000 USDC.

# Right
No transfers over 1000 USDC, except to the emergency reserve wallet (0xABC...).

Bare assertions

A bare assertion is a rule with no condition, like The transfer is not permitted. Without a condition, this creates an axiom that is always true, causing the solver to return IMPOSSIBLE for any action involving that variable. Reserve bare assertions only for boundary conditions.

# Wrong
The action must be rejected.

# Right
If the transfer justification source is a social media post, then the action must be rejected.

# Boundary conditions are fine as bare assertions
The transfer amount must be greater than zero.
The transfer amount must not exceed the total wallet balance.

Missing boundary conditions

The solver does not assume numeric values are positive or within any particular range. If your policy has a threshold rule, anchor it with explicit bounds or you may get unexpected SATISFIABLE results for edge cases like zero-value transfers.

Boolean variables with only one state defined

When your policy introduces a boolean concept, write rules for both states. If you only write the blocking condition, the solver has no information about what the permitted state looks like.

# Wrong
If human confirmation has not been received, then the transfer is not permitted.

# Right
If human confirmation has been received and logged, then the transfer may proceed subject to other rules.
If human confirmation has not been received, then the transfer is not permitted.

Enumerated values in a single rule

Write one rule per discrete value. Bundling them into a list risks one value being dropped during translation.

# Wrong
If the justification source is a social media post, messaging platform, or on-chain data, then the transfer is not permitted.

# Right
If the justification source is a social media post, then the transfer is not permitted.
If the justification source is a messaging platform, then the transfer is not permitted.
If the justification source is on-chain data, then the transfer is not permitted.

---

Formalizing social engineering defenses

Numeric and registry rules are straightforward to formalize. Social engineering defenses — urgency appeals, emotional manipulation, false authority claims — require a different approach: explicit boolean variables.

Rather than relying on the solver to infer what "emotionally manipulative" means, name each attack vector as a first-class policy variable.

Agentic Treasury Protection Policy

The maximum single transfer is 100 tokens.
Transfers are only permitted to addresses in the approved recipient registry.
If the transfer instruction contains an emotional appeal, then the transfer is not permitted.
If the transfer instruction contains an urgency tactic, then the transfer is not permitted.
If the transfer instruction contains a sob story, then the transfer is not permitted.
If the transfer instruction claims pre-authorization from an external source, then the transfer is not permitted.
If the wallet balance at the time of instruction is unknown, then the transfer is not permitted.

This formalizes hasEmotionalAppeal, hasUrgencyTactic, hasSobStory, and hasExternalAuthorityClaim as boolean variables the solver evaluates alongside the numeric and registry rules. Neither social engineering nor technical bypass changes the math.

---

Testing before deploying

Use /v1/checkIt to test your policy with a range of actions before wiring it into a live agent. Each check costs 1 credit.

Boundary testing. If your policy blocks transfers over 1000 USDC, test exactly 999, 1000, and 1001. The boundary is where enforcement is most likely to fail.

Adversarial testing. Try phrasing actions the way a bad actor might: vague descriptions, split transactions designed to stay under limits, urgency framing, authority claims.

Missing-field testing. What happens if a required field is absent? A well-written policy should fail closed. If your policy requires a confirmed wallet balance, test an action that does not mention the balance at all.

Enumeration testing. For every discrete value your policy names, test one action containing that exact value. Do not assume the solver generalizes across synonyms.

Contradiction hunting. If the solver returns IMPOSSIBLE on a reasonable action, two rules are likely conflicting. Revisit your policy for overlapping or contradictory constraints.

---

Policy versioning

Every call to /v1/makeRules produces a new policy_id. Treat these like code and keep a record of each version. To roll back, switch the policy_id your agent passes to /v1/checkIt.

Good practice is to maintain at least three versions: production, staging, and draft. Test changes in staging before promoting to production.