Catching Edge-Case Bugs Early with TLA+ and Statecharts

Introduction When you write code with Coding Agent (Claude Code in this case), you normally write unit, integration and end-to-end tests to prevent some of future feature implementation or bug fix, or refactor codes effects to the current behaviors of the application. But what about edge-case bugs? We don't know how to catch those kind of bugs until you know and write a test case for it based on domain logic or it happened in the production environment, and you treat it as a bug and try to fix it after it happen. But what about catching and fixing it during the time you implement the feature? When you implement the application logic, it normally works like a logic flow or state machine, right? And with the state machine, you can let the coding agent detect all the flows for you. If it is an explicit flow, then it's easy because you can check it in the code yourself or even the coding agent can catch and fix it. But what about the implicit flow? It's normally we don't know what we don't know! But at the end of this Oct, 2026, Steve Ruiz twitted one prompt which is viral in the internet, because it is really smart to explore all the implicit state machine of the application. It's short and smart, which forces the coding agent to search and explore all the implicit flow in the app. And I want to try it with coffeeshop-jev app which I'm developing by coding agent last month. For those who don't know, it is a coffeeshop domain which allows humans to buy a coffee at the counter agent, processes items (drink and food items), sends them to the barista and kitchen agents to cook, and responds back to the human about the status. It maintains the workflow, which allows the agent and human to have a conversation to order the drink/food items. And it built with multiple agents architecture (workflow) on top of Microsoft Agent Framework. And its flow is: And with this flow, I ran it and found no bugs; the flow worked normally. But I suspect it might contain some edge-case bugs which I didn't know about when I read the diagram above. I decided to try the method from Steve above to explore. I opened up the terminal with Claude Code and typed find all of the implicit state machines in my app: And even better, suggest some bugs in my app: Now the problem is that I know about the bug from the text from Claude Code, but it is hard for me to grasp the flow. I saw In the Finish handler of the AG-UI path, an Extract failure still counts toward the cap: ClarifyRequest when working.Asks >= MaxAsks. The comment says Gate-only counting was a bug. And I was looking for some method to visualise these in a diagram; then I fixed it and made sure this bug will not happen again in the future. And last night, I came across Lauren Tan (@potato) tweet coincidentally, and it fit what I wanted for the scenario above. How can I do it? In the terminal with Claude Code in the current session, I typed use /create-formal-verification-skill to model these state machines, one skill per subsystem. And use /statechart to visualise my most important user flows (this is exactly what Lauren said in the tweet; nothing magic here. But you make sure to install pstack at https://github.com/cursor/plugins/tree/main/pstack) And some other text in the terminal (I don't show it here because of brevity). But the main point is that it created 3 more skills: verify-ask-loop, verify-answer-channel, and verify-fulfilment. And in this result, I see 1 flow contains a bug: ask-loop. But there are some TLA files pointed to in these skills as well. TLA+ TLA+ stands for Temporal Logic of Actions. TLA+ is a high-level, formal specification language created by Leslie Lamport. It is designed specifically for modelling and verifying concurrent and distributed systems—such as multi-threaded applications, consensus algorithms, and cloud databases—by describing what a system should do rather than how the code is written. And yes, we leverage a coding agent to help us scan, explore and generate the TLA+ for our app. And from there, we can generate the state chart to visualise the bugs - how fantastic is it! And when I copy the ask-loop state chart to the Mermaid Live Editor: Have you seen the red and yellow boxes? It is a bug, and the affected flow is affected by this bug. Now I will fix it using Claude Code: fix finding 1 pls: And, Now, I run the app again to make sure it's still working: aspire run, wait a bit, then go to http://localhost:5200, and type text to order as below: Conclusion This post demonstrates that we can use formal verification with TLA+ to detect, explore and fix edge-case bugs very soon, even in the implementation phase. This is especially important when you rely heavily on a coding agent to implement almost everything for you. And yes, verification has become important now. Happy hacking!