@txfence/verify

Formal verification and adversarial stress testing for txfence policies. Catches policy misconfiguration before deployment.

Installation


npm install @txfence/verify

Formal verification

Three properties can be verified:

absolute_cap_reachability

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


import { verify } from '@txfence/verify'
 
// verify() is synchronous — properties take cap/token/maxSpendPerTx directly
const result = verify({
  kind:                 'absolute_cap_reachability',
  agentCount:           10,
  transactionsPerAgent: 10,
  capAmount:            50_000n * 10n ** 6n,
  token:                'USDC',
  maxSpendPerTx:        1_000n * 10n ** 6n,
})
// result.status:        'holds' | 'violated' | 'unknown'
// result.property:      string identifier of the checked property
// result.counterExample — minimal counterexample when violated

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,
  capAmount:            25_000n * 10n ** 6n,
  token:                'USDC',
  maxSpendPerTx:        1_000n * 10n ** 6n,
})

policy_containment

Is every action allowed by innerPolicy also allowed by outerPolicy?


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

Adversarial stress testing

Six default attack vectors tested against the policy (a seventh, chain_reorg, exists in the type but is not in DEFAULT_VECTORS — opt in via the vectors option):


import { stressTest } from '@txfence/verify'
 
const report = await stressTest(policy, {
  agentCount:              10,
  transactionsPerScenario: 20,
})
 
console.log(report.survivalRate)
console.log(report.recommendation)

Six default vectors: rapid_fire, coordinated_drain, rpc_failure, stale_simulation, cap_boundary, approval_flood.

RiskReport includes: policy, totalScenarios, survived, failed, survivalRate, failedScenarios, byVector, bySeverity, generatedAt, durationMs, recommendation.

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
txfence stress-test --config ./txfence.config.ts --agents 10 --transactions 20

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

Important

Bounded verification only. A property that holds for N=10, M=10 may still be violated for larger values. Document your bounds.