SELECTED WORK / 03 / BOUNDED RUST PROJECT
TxProof.
Make the failure case reproducible.
ILLUSTRATIVE TRACE FROM AN EXECUTABLE REGRESSION · BOUNDED TEST CASE
Turn uncertainty into a replayable case.
Rust tooling for bounded counterexample search across money-moving backend invariants, using a synthetic payment reference application.
01 / THE PROBLEM
What made this hard
A provider can commit a payment operation and lose the response before the caller knows its result. A changed retry identity may create another object even though the first call succeeded.
02 / ROLE & CONSTRAINTS
What I owned
Built the Rust campaign planner, runtime safety boundaries, PostgreSQL invariant runner, and replay/evidence path in a self-directed public project.
Search is bounded to state-valid cases, test databases must be disposable and identity-checked, and a reported counterexample must have inspectable evidence.
03 / DECISIONS
How the boundary works
- 01
Generate bounded schedules covering retries, ambiguous provider results, webhook delay/drop/reordering, and crash/restart cut points.
- 02
Persist decision streams so a violating case can be replayed against a compatible fresh test baseline.
- 03
Bind destructive reset acknowledgement to exact database and project identity, and evaluate SQL invariants in one read-only repeatable-read snapshot.
04 / FAILURE CASE
The case worth testing
In the synthetic commit-then-close case, a retry with a changed idempotency key yields two provider objects and violates provider-object-unique. Keeping the same key yields one object in the paired corrected case.
05 / PROOF & LIMITS
What the evidence supports
The public configured-run regression asserts the violating and corrected outcomes. Workspace tests passed in the audit, and the isolated reference-app CI job succeeded on 25 August 2026.
Bounded search against a repository-owned reference app and fixture provider. No formal proof of arbitrary payment systems, live Stripe boundary, or customer deployment is claimed.
TOOLS & TECHNOLOGIES