Formal Verification

@txfence/verify provides bounded model checking for policy invariants. Given a policy and bounds, it either proves the property holds or produces a concrete counterexample showing how it can be violated. Use it in CI to catch policy misconfiguration before deployment.

Installation


npm install @txfence/verify

Three properties

absolute_cap_reachability

Can N agents × M transactions reach or exceed the absolute cap?


import { verify } from '@txfence/verify'
 
// verify() is synchronous — it returns a result immediately, no await needed
const result = verify({
  kind:                 'absolute_cap_reachability',
  agentCount:           10,
  transactionsPerAgent: 10,
  capAmount:            50_000n * 10n ** 6n,   // 50,000 USDC
  token:                'USDC',
  maxSpendPerTx:        1_000n * 10n ** 6n,    // 1,000 USDC per tx
})
 
if (result.status === 'violated') {
  console.error('Cap can be exceeded:', result.counterExample)
}

Arithmetic check: agentCount × transactionsPerAgent × maxSpendPerTx vs capAmount. Generates the minimal counterexample — only the transactions needed to exceed the cap. Properties take cap/token/maxSpendPerTx directly rather than a full Policy so the checker can be exercised against hypothetical values without constructing a complete config.

rolling_window_saturation

Can N agents collectively exceed a rolling window cap through adversarial scheduling?


const result = verify({
  kind:                 'rolling_window_saturation',
  agentCount:           5,
  transactionsPerAgent: 20,
  windowMs:             3_600_000,            // 1 hour
  capAmount:            25_000n * 10n ** 6n,  // 25,000 USDC rolling cap
  token:                'USDC',
  maxSpendPerTx:        1_000n * 10n ** 6n,
})

Tests four adversarial scenarios: simultaneous burst, staggered burst, double burst, worst-case single agent. Counterexample shows exact timestamps and amounts that cause the violation.

policy_containment

Is every action allowed by innerPolicy also allowed by outerPolicy?


const result = verify({
  kind:        'policy_containment',
  innerPolicy: stricterPolicy,
  outerPolicy: broaderPolicy,
})

Uses createTestActions + diffPolicies internally. Flags newly_rejected actions as containment violations. Use this to verify that tightening a policy doesn’t accidentally block actions that should still be allowed.

VerificationResult


type VerificationResult =
  | { status: 'holds';    property: string; checkedBound: CheckBound; scenariosChecked: number; durationMs: number }
  | { status: 'violated'; property: string; counterExample: CounterExample;                     durationMs: number }
  | { status: 'unknown';  property: string; reason: string;                                     durationMs: number }
 
type CheckBound = {
  agentCount:           number
  transactionsPerAgent: number
  windowMs?:            number
}

CounterExample


type CounterExample = {
  description:    string
  transactions:   TransactionScenario[]
  violatedAt:     number
  violatedAmount: bigint
  capLimit:       bigint
  checkedBound:   CheckBound
}
 
type TransactionScenario = {
  agentId:   string
  action:    Action
  timestamp: number
  amount:    bigint
}

verifyAll

Run multiple properties in parallel. verifyAll is async (wraps each sync verify() call in a resolved Promise) so consumers get a single await instead of N synchronous checks.


import { verifyAll } from '@txfence/verify'
 
const results = await verifyAll([
  {
    kind:                 'absolute_cap_reachability',
    agentCount:           10,
    transactionsPerAgent: 10,
    capAmount:            50_000n * 10n ** 6n,
    token:                'USDC',
    maxSpendPerTx:        1_000n * 10n ** 6n,
  },
  {
    kind:                 'rolling_window_saturation',
    agentCount:           5,
    transactionsPerAgent: 20,
    windowMs:             3_600_000,
    capAmount:            25_000n * 10n ** 6n,
    token:                'USDC',
    maxSpendPerTx:        1_000n * 10n ** 6n,
  },
])

CLI


txfence verify absolute-cap   --config ./txfence.config.ts
txfence verify rolling-window --config ./txfence.config.ts
txfence verify policy-contains --config ./txfence.config.ts
 
# JSON output
txfence verify absolute-cap --config ./txfence.config.ts --json

All commands exit 0 when the property holds, 1 when violated — CI-friendly.

Bounded verification only. A property that holds for N=10, M=10 may still be violated for larger values. Always document your bounds. A Z3 SMT backend for complete proofs is planned.