pen-to-squareWriting 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.

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.


Common mistakes

Relative terms without definitions

Bundling multiple constraints

Process language instead of constraint language

Conflicting rules

Implicit exceptions

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.

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.

Enumerated values in a single rule

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


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.

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.

Last updated