Emery Coxe

Chief Architect

First Dollar

Roadblock Title:

Proving Financial State Machines Correct: TLA+, Mutation Testing, and Property-Based Testing in Production

Time:

Tuesday - 2:00 PM (Tower B)

Abstract:

Our ledger has five settlement states. Our funding pipeline has seven. Our claim lifecycle has nine. A wrong transition means money in the wrong place. Traditional tests check the paths you thought of — we wanted to check the ones we didn’t. At First Dollar, we write TLA+ specs for financial state machines and run the model checker in CI on every PR. We use mutation testing to prove our tests catch bugs — our initial score was 51%, meaning half of injected faults went undetected. We use property-based testing to find edge cases humans miss. This talk covers how all three work in production on real money-moving code, what each catches that the others don’t, and why financial state machines justify this level of rigor.

Bio:

Emery Coxe is a systems thinker and hands-on engineer, leading high-performing teams and scaling enterprise-level applications. As the Chief Architect at First Dollar, he oversees innovation and research efforts with a focus on applications of AI and ML. Emery is based in Austin, TX, and when not working, he enjoys lifting weights, playing drums in garage bands, and spending time with his wife and baby daughter Betsy.