AWS Builder Center

Builder Center

How we built a formally verified fraud rules engine on AWS

Formally verified fraud rules on AWS: Z3 proves correctness before deploy, Cedar enforces bypass-proof hard-stops at runtime, Drools handles stateful velocity rules. Plus UORF — an open format for translating rules across 8 platforms.

Faris Haddad - AWS

Data and Ai lead at AWS
Every financial institution runs a rules engine. Somewhere in your technology stack there is a list of conditions — IF the beneficiary country is on the FATF high-risk list AND the amount exceeds £1,000 THEN block the transaction. For most teams, the confidence that these rules work correctly comes from testing. You write test cases. You add edge cases after incidents. You run the suite before each deploy.
This post argues that testing is not enough — not because testing is poorly done, but because of what testing structurally cannot tell you. It cannot tell you whether a rule can ever fire at all. It cannot tell you whether a sophisticated attacker could construct a transaction that navigates through your rulebook without triggering any block. And it cannot tell you whether two rules that are supposed to be mutually exclusive can actually co-fire on some input no one thought to test.
We encountered all three failure modes when we built the Fraud Rule Engine. This post explains the architecture we used to solve them — three layers, three tools, each providing a guarantee the others cannot.


The three problems with testing-only rule governance

Dead rules. A rule can be syntactically valid and semantically broken. A condition like  aws:SourceVpce StringEquals "*"  in an IAM policy looks like a wildcard, but  *  is a literal string, not a glob. The policy effectively never matches anything. As Neha from the AWS Automated Reasoning Group demonstrated in  ARG: How AWS Service Teams use Automated Reasoning for Security , even experienced security engineers looking at such policies can miss the issue. The same pattern occurs in fraud rules: a condition that looks like it fires on all wire transfers, but due to a type mismatch or an off-by-one, never does. Testing only catches dead rules when you explicitly test for the case that should fire.
Bypass chains. In a tiered rules engine, Tier 1 rules should block before Tier 2–4 rules evaluate. But if salience is misunderstood — it controls evaluation order, not prevention of execution after a fact insert — a Tier 3 rule might fire after a Tier 1 block has already been issued. The transaction gets a secondary decision that shouldn't exist. No test catches this unless you specifically constructed a scenario that exercises the exact interaction.
Rule interaction violations. Two rules designed to be mutually exclusive — one fires for card fraud, one for AML structuring — may actually share a satisfying input. A transaction that triggers both produces an ambiguous outcome. In a system with 27+ rules across multiple channels, the combinatorial space of possible interactions is enormous. A test suite covers the cases you anticipated. It says nothing about the cases you didn't.


The three-layer model

The Fraud Rule Engine (FRE) addresses these three problems with three independent layers, each providing a guarantee the others cannot:
Plain text
PRE-DEPLOYMENT          RUNTIME TIER 1          RUNTIME TIERS 2–4
─────────────────       ─────────────────       ─────────────────
Z3 Theorem Prover  →    Cedar / AVP         →   Drools Rete (ECS)
Mathematical proof       Structural hard-stop    Stateful evaluation
before any deploy        sub-ms, every txn       velocity + aggregation

The integration contract is minimal: transactions arrive on an  Amazon Kinesis  data stream ( fre-transaction-stream ) enriched with velocity signals and risk attributes. Decisions are emitted to an  Amazon EventBridge  bus ( fre-decision-bus ). No changes to the host fraud platform are required.


The intellectual foundation: why automated reasoning?

In 2018, Byron Cook — founder and director of the AWS Automated Reasoning Group — published the first public description of Zelkova, an internal AWS service that uses automated reasoning to analyze IAM policies. Zelkova now powers  IAM Access Analyzer for S3 ,  AWS Config  managed rules,  Amazon Macie ,  Amazon GuardDuty , and several other services. Cook described the capability this way in 2025: "I brought this sort of capability to Amazon starting about 10 years ago."
The insight behind Zelkova — and behind the FRE's Z3 layer — is that policies are logical formulas. An IAM policy statement can be translated into a mathematical expression over variables (principal, action, resource, conditions). A fraud rule is the same structure: a formula over transaction attributes. Once you have a formula, you can use an SMT solver to ask questions about it over the entire input space, not just the test cases you thought to write.
Zelkova uses this to answer: "Is this S3 bucket publicly accessible?" The FRE uses the same technique to answer: "Can this tier-gate be bypassed? Can this rule ever fire? Can these two rules co-fire when they shouldn't?"
The tool is  Z3  — Microsoft Research's open-source SMT (Satisfiability Modulo Theories) solver, licensed under MIT. Z3 takes a logical formula and either proves it is true for all possible values of the variables, or returns a counterexample: concrete values that make it false. The counterexample is the part that makes this actionable in practice. When Z3 finds a bypass chain, it doesn't just say "there's a problem" — it returns the exact transaction attributes that exploit it.


Building block 1: Z3 formal verification

Architecture

The Z3 Prover runs as a Docker  AWS Lambda  function (1,024 MB, 5-minute timeout). It is invoked as a gate in the deploy pipeline — before any rulebook change reaches production. Proof artefacts are written to  Amazon S3  for regulatory audit.

What it checks

We run five categories of proof on every deploy. We label these I1–I5 for reference — the underlying SMT operations are standard satisfiability queries, but the taxonomy is our own:
Label
Check
What Z3 proves
I1
Joint satisfiability
Can two rules that shouldn't co-fire simultaneously actually do so?
I2
Bypass chains
Can a lower-tier action execute after a higher-tier block has been issued?
I3
Outcome amplification
Do two rules together produce a more severe outcome than either alone intended?
I4
Mutual exclusion
Are supposedly exclusive rules provably exclusive over all inputs?
I5
Dead rules
Is there any valid input that makes this rule fire at all?

Results from the first run

Against 27 rules, Z3 returned 63 findings. Most were I5 dead rules (conditions that could never be satisfied together) and I2 bypass chain risks. None were "bugs" in the traditional sense — they were proof obligations the human authors hadn't explicitly reasoned about. The most instructive finding was the interaction between ATO-UNIFIED (the cross-product account takeover rule, salience 1100) and WT-005 (dormancy spike, salience 900). Z3 flagged this as  I1_JOINT_SAT CRITICAL : both rules share a satisfying input. This is the correct finding — ATO-UNIFIED is designed to co-fire before WT-005, with a structural tier gate preventing WT-005 from executing if ATO-UNIFIED has already blocked. The Z3 finding confirmed the structural gate was necessary. Without the  not FraudDecision(action == "BLOCK")  condition in WT-005, both rules would produce decisions on the same transaction.


Building block 2: Cedar and Amazon Verified Permissions

Why Cedar for fraud compliance?

Testing validates the cases you anticipated. Cedar's forbid-wins semantics provide a structural guarantee independent of testing. If any  forbid  policy matches a transaction, the decision is  DENY  — unconditionally, regardless of how many  permit  policies also match. This is not a configuration option. It is the language definition, as specified in the  Cedar policy language reference .
The distinction matters for compliance: you can tell a regulator that a sanctions check cannot be bypassed because the authorization language's evaluation procedure makes it structurally impossible, not because a test suite says so.

Cedar on AWS: choosing the right service

Cedar is available via two distinct AWS services. Choosing the wrong one is a common mistake:
 Amazon Verified Permissions (AVP)  launched GA on June 13, 2023. It is purpose-built for application-level fine-grained authorization — RBAC/ABAC for users, accounts, and domain entities. It is fully supported by  AWS CloudFormation  and  Terraform . The principal is your application's user or account. The resource is your application's data or transaction. This is the right choice for the FRE: we are authorizing financial transactions, not constraining LLM agent behavior.
Policy in Amazon Bedrock AgentCore uses Cedar to constrain what AI agents can invoke through the AgentCore Gateway. As explained in  Why Policy in Amazon Bedrock AgentCore chose Cedar for securing agentic workflows , the enforcement point is the Gateway intercepting every MCP tool call before it reaches the tool. The IaC resource is  CedarPolicy  in the AgentCore Control Plane API. This is the right choice when the thing you're constraining is an LLM agent, not a payment. Cedar recently joined the CNCF as a Sandbox project (December 2025), reflecting its growth as an open authorization standard beyond AWS.
For a complementary perspective on Cedar in financial services — specifically applying it to LLM decision governance — see  Defense-in-depth governance for LLM decisions on AWS Bedrock . The architectural insight is consistent: Cedar provides the deterministic enforcement layer that the LLM itself cannot be trusted to enforce.

The 5 + 1 policy design

The FRE's AVP policy store holds exactly six policies: five  forbid  statements and one catch-all  permit . The count is fixed — no additions without a security review. Velocity-based rules never go in Cedar; they require enrichment signals (velocity counts, account history) that Cedar cannot access because it evaluates each request statelessly.
cedar
// WT-003: FATF High-Risk Jurisdiction
forbid (
    principal,
    action == FRE::Action::"wire_transfer",
    resource
)
when {
    ["IR", "KP", "MM", "SY", "YE",
     "LY", "SO", "SS", "CF", "CD",
     "HT", "RU", "VE", "PK", "AF"].contains(resource.beneficiaryCountry) &&
    resource.amountGbp > 1000
};

The catch-all  permit  at the bottom is essential. Cedar is default-deny — without an explicit permit, every transaction would be blocked. The  permit  says: if none of the five  forbid  policies matched, Cedar has no structural objection. The transaction proceeds to Drools.

The deployment lesson that cost us a day

Set membership in Cedar uses  [list].contains(x) . The expression  x in [list]  looks like it should work, but  in  is Cedar's entity-hierarchy operator — it tests whether an entity is a descendant of another entity's hierarchy. It does not perform scalar set membership.  resource.beneficiaryCountry in ["IR","KP"]  fails AVP STRICT validation at policy write time.  ["IR","KP"].contains(resource.beneficiaryCountry)  is correct. This is confirmed in the  Cedar language reference . Test your policies locally with the Cedar CLI before pushing to AVP.


Building block 3: Drools Rete on ECS Fargate

Why stateful rules need a different engine

Cedar evaluates one request at a time against static attributes. It cannot count how many wire transfers an account has made in the last 24 hours, because it has no access to transaction history. Rules that require  COUNT_LAST ,  SUM_LAST , or multi-event patterns — card testing velocity, structuring detection, account takeover signals — need a stateful engine with Working Memory.
The Fraud Rule Engine uses  Drools 10  running on  Amazon ECS  Fargate (Java 17, Spring Boot 3.2.5, 2 vCPU / 4 GB, auto-scaling 2–10 tasks at 70% CPU).

The Rete algorithm and why it matters for large rulebooks

Rete is a pattern-matching algorithm for efficiently evaluating large sets of rules against a changing set of facts. Its key property: instead of re-evaluating every rule from scratch when a new fact arrives, Rete builds a compiled network of condition nodes that share partial matches. When 12 of your 27 rules share the condition  transactionType == "WIRE_TRANSFER" , that condition is evaluated once and its result is shared across all 12 rules simultaneously.
For a 27-rule catalogue this is a modest efficiency gain. For a 500-rule production rulebook, Rete's partial-match sharing is 10–100× faster than naive sequential evaluation.

The salience / not() distinction

Important:  salience  controls evaluation order — which rule fires first when multiple rules are active simultaneously. It does not structurally prevent a lower-tier rule from executing after a higher-tier block has been inserted.
The structural tier gate is the  not FraudDecision(transactionId == $tx.id, action == "BLOCK")  negative condition. Once a BLOCK  FraudDecision  fact exists in Working Memory, this condition prevents lower-tier rules from activating. Salience ensures the BLOCK fires first;  not()  ensures lower tiers see the result.
Java
// salience 800 = evaluation order (fires after Tier 1)
// not FraudDecision(action == "BLOCK") = structural gate
//   → this rule cannot activate if a BLOCK decision already exists
rule "WT-002: Structuring Pattern"
salience 800
when
    $tx   : Transaction(transactionType == "WIRE_TRANSFER")
    $acct : AccountFacts(
        accountId      == $tx.accountId,
        wireCount24h   >= 3,
        wireSum24h     > 9000,
        wireMaxAmount24h < 3500
    )
    not FraudDecision(transactionId == $tx.id, action == "BLOCK")
then
    insert(new FraudDecision($tx.id, "FLAG", 80, "AML_STRUCTURING",
        "WT-002: Structuring pattern detected"));
end

The canonical account takeover chain shows how this composes across tiers:
Plain text
ATO-UNIFIED  (salience 1100, BLOCK)  → fires first, inserts BLOCK into Working Memory
WT-005       (salience 900,  FLAG)   → not() prevents activation, gated
ACH-003      (salience 900,  FLAG)   → not() prevents activation, gated



Building block 4: UORF and the rule generator

The portability problem

Fraud rules are trapped in proprietary formats. SAS FM rules are SAS procedural code. FICO Blaze Advisor rules are YAML. NICE Actimize rules are SQL-like scenario DSLs. Oracle OFSAA rules are parameterized SQL stored in a metadata repository. Moving a rule from one platform to another means re-authoring it from scratch in a new syntax. There is no prior standard for a platform-neutral fraud rule interchange format — no IETF RFC, no OASIS standard, no OMG specification.

Unified Open Rule Format (UORF)

UORF (Unified Open Rule Format) is an open JSON schema developed for this project (Apache 2.0, August 2026) that expresses any fraud rule independently of the target engine. A rule authored in UORF can be translated to any of eight target formats:
Format
Platform
Cedar (AVP)
Amazon Verified Permissions
Drools DRL
Drools Rete Engine
SAS FM
SAS Fraud Framework
FICO Blaze
FICO Blaze Advisor
Actimize DSL
NICE Actimize
IBM JSON
IBM Safer Payments
OFSAA SQL
Oracle OFSAA AML
Featurespace
Featurespace ARIC (Visa, 2023)
A UORF rule carries a  pattern_type  that determines which engine it routes to. Rules with  pattern_type: stateless_block ,  tier: 1 , and no temporal window are Cedar-eligible. Everything else routes to Drools.
JSON
{
  "id": "WT-003",
  "tier": 1,
  "pattern_type": "stateless_block",
  "conditions": [
    { "field": "beneficiaryCountry", "op": "in", "value": ["IR","KP","MM","SY"] },
    { "field": "amountGbp", "op": "gt", "value": 1000 }
  ],
  "action": "BLOCK",
  "salience": 1000,
  "queue": "SANCTIONS_COMPLIANCE"
}

The rule generator ships with 92 canonical patterns across 8 fraud families — Wire Transfer, Cheque Fraud, ACH, Debit Card, Credit Card, ATO/Cross-cutting, Generic Composite, and Emerging Threats (APP scams, deepfake-enabled ATO, mule network graph detection, synthetic identity lifecycle). You can try it at  https://dq3vhygcbo48u.cloudfront.net .


Deployment lessons

Five things that broke during the initial deployment, and what actually fixed them:
1. Cedar on AWS: choose the right service. We initially built against "AgentCore Policy (Cedar)" resources. For transaction authorization,  Amazon Verified Permissions  is the correct service — it is the purpose-built Cedar authorization service for application-level RBAC/ABAC with CloudFormation and Terraform support.
2. Cedar set membership syntax.  x in [list]  fails AVP STRICT validation —  in  is an entity-hierarchy operator. Use  [list].contains(x) .
3. ARM Mac → ECS Fargate architecture mismatch. Building Docker images on an Apple Silicon Mac produces ARM64 images. Fargate expects x86_64. Build flags:  --platform=linux/amd64  in the Dockerfile and in the CDK asset bundling configuration.
4. Drools 10 MVEL crash. Root cause: missing  org.drools:drools-mvel  JAR. Setting  -Ddrools.parallelRulesBuildThreshold=-1  disables parallel builds and masks the symptom. The correct fix is explicitly adding  drools-mvel  to the classpath or migrating to Drools' executable model, which deprecates MVEL in Drools 10.
5. Python wheels in Lambda.  pydantic_core  is a Rust binary wheel. A wheel installed on an ARM Mac will not load on Lambda's x86_64 Linux runtime. Either cross-compile with  --platform manylinux2014_x86_64 --only-binary :all: , or eliminate the Pydantic dependency and use stdlib-only code — which is what we chose for the Rule Generator Lambda.


Prerequisites

To explore the deployed version of this system:
  • For the Drools engine: Java 17+, Maven 3.9+
To deploy the Fraud Rule Engine yourself:
  1. Clone  github.com/farishaddad/Fraud-Rule-Engine 
  1. Install prerequisites: Node.js 18+, AWS CDK v2, Python 3.12, Java 17, Terraform 1.5+
  1. Follow the deployment order in  docs/DEPLOYMENT_RUNBOOK.md : CDK stack → Cedar (Terraform) → CI/CD pipeline → UI
  1. Run  pytest packages/rule-generator/tests/  to verify the 884-test suite passes locally before deploying


What's next: Dogwood and temporal Cedar

The blog so far describes a clean split: Cedar handles stateless hard-stops, Drools handles stateful velocity rules. That split exists because Cedar — as deployed in Amazon Verified Permissions today — evaluates one request at a time with no access to transaction history. A card-testing rule checking "5+ transactions in 1 hour" requires a running count, which means Drools Working Memory.
AWS  Dogwood  changes this equation. Dogwood is a governance language that extends Cedar with temporal conditions —  formerly within 1h ,  since ,  once , and windowed aggregations over an event history. It compiles down to standard Cedar; the temporal predicates become  context.*  slots that a temporal engine fills at runtime from the event trace.
Here is DC-001 (card testing velocity) expressed in Dogwood, compared with the Drools DRL version:
Dogwood:
Plain text
@id("dc001_card_testing")
forbid (
    principal,
    action == FRE::Action::"card_purchase",
    resource
)
when { context.input.avgAmount < 5.00 }
when temporal {
    count(formerly within 1h FRE::Action::"card_purchase"::request{
        input.cardId: context.input.cardId
    }) >= 5
};

Drools DRL (current):
Java
rule "DC-001: Card Testing Velocity"
salience 1000
when
    $tx   : Transaction(transactionType in ("POS_PURCHASE","CNP_PURCHASE"))
    $card : CardFacts(
        cardId         == $tx.cardId,
        txCount1h      >= 5,
        avgTxAmount1h  < 5.00,
        declinedCount1h >= 2
    )
then
    insert(new FraudDecision($tx.id, "BLOCK", 91, "CARD_FRAUD_PRIORITY",
        "DC-001: Card testing pattern"));
    modify($card) { setCompromiseFlag(true); }
end

The Drools version requires: a pre-enrichment Lambda computing  txCount1h  and  avgTxAmount1h  into DynamoDB, a Redis compromise-flag store, and a Java ECS service running the Rete engine. The Dogwood version requires: only the policy and an event trace — the temporal engine evaluates the count directly from the transaction history.
In  Amazon Bedrock AgentCore , Dogwood temporal policies are evaluated natively inside the AgentCore Gateway. Session trajectories are maintained automatically with a 24-hour lookback — covering the majority of fraud velocity windows (card testing = 1h, structuring = 24h, wire bursts = 24–48h). No custom temporal engine, no DynamoDB velocity table, no Enrichment Lambda — for these rule types.
What stays in Drools with Dogwood:
  • Rules with >24h lookback (90-day dormancy detection for ATO-UNIFIED)
  • Multi-entity graph patterns (mule network detection — fan-in/fan-out across accounts)
  •  modify()  fact propagation (DC-001 setting a compromise flag that DC-005 reads on the next transaction)
What could migrate to Dogwood:
  • All velocity/count rules within 24h windows (~12 of the 22 Drools rules)
  • Amount-sum aggregation rules (structuring detection)
  • Sequential event patterns (login → password reset → wire transfer within 10 minutes)
The architectural implication: the three-layer model becomes two layers for most rules — Z3 (pre-deploy proof) and Cedar + Dogwood (runtime enforcement with temporal awareness). Drools stays only for the 7–10 rules that genuinely need cross-entity graph traversal or long-horizon state.
This is the direction we're taking the Fraud Rule Engine next: migrating velocity rules from Drools DRL to Dogwood temporal policies, unified under one Cedar-derived language, deployed to AgentCore Policy. The UORF rule generator already emits Cedar; adding a Dogwood emitter to produce temporal policy output is a natural extension.


Conclusion

Three tools, three guarantees:
  • Z3 proves correctness before deployment across the entire input space. Testing cannot do this.
  • Cedar makes compliance blocks structurally bypass-proof at runtime. Testing cannot do this either.
  • Drools Rete evaluates stateful velocity, temporal, and multi-event rules with Working Memory. Cedar cannot do this.
Each layer handles what the others cannot. None of them replaces the others. Together, they make fraud rule governance something you can reason about formally rather than test exhaustively.
The project is open source under Apache 2.0. Contributions to the UORF pattern catalogue — particularly patterns from non-UK payment channels — are welcome.


Related reading



Cleanup

If you deployed the FRE stack to explore it, remove resources to avoid ongoing charges:
Bash
# Remove Cedar policy store (Terraform)
cd packages/cedar-policy/avp
terraform destroy -var="env=prod" -var="region=us-east-1"

# Remove CDK infrastructure
cd infrastructure
npx cdk destroy --all

The  Amazon ECS  Fargate tasks,  Amazon Kinesis  stream,  Amazon DynamoDB  velocity table, and  Amazon ElastiCache  Redis cluster will all be removed by the CDK destroy.
# ai-security# agentic-ai# financial-services# machine-learning# amazon-bedrock
Any opinions in this article are those of the individual author and may not reflect the opinions of AWS.
Enjoyed reading this content? Let the author know!

Your likes, comments, shares, and saves help creators reach more builders.

Loading recommendations

Loading article