I indirectly use TLA+ through https://github.com/quint-co/quint. I added instructions that "before you implement any feature, please use Quint to model it and make sure no counterexample for the system as a whole, reiterate the design with Quint as well and make sure your documents and implementation follows the formal model and docs".

The result, while takes much longer, is quite magical. A lot of transaction and atomic bugs were found and fixed just by having such simple instruction alone.

However, sometimes it is not all magical especially around external resources. Cloudflare, unfortunately, sometimes have hiccups on D1 and KV with timeout, which is more or less a force majeure.

Fortunately, that means I will have to model the action as a binary event, that the transaction may not complete as we would have thought guaranteed, and by add extra guard around it, so that the state would have to be retried.

I was able to workaround it like that so far. Keep in mind the more conditions and constraints, the beefier your CPU might need since it is on the scale of NP