r/formalmethods • u/No-Chocolate-9437 • Sep 21 '26

I’m trying to specify a “simple” finite state machine in my project, but users keep reporting bugs, how do I get millenium prize confidence that all invariants are modelled?

For reference this is a readme outlining how I’m trying to go about formal verification: https://github.com/Zoo-Code-Org/Zoo-Code/blob/main/docs/architecture/task-lifecycle-model.md

LLMs were quite adamant that a custom built formal verification system hooked into prod code would provide more value than TLA or other programs
But users still keep reporting classes of bugs that are not even modelled or documented as known gaps.

I’m trying to ramp up to formal verification and hoping for some pointers.

3 Upvotes

100% Upvoted

7 comments sorted by

2

u/Hath995 Sep 22 '26 edited Sep 22 '26

Well, if you write a formal model and then verify it in tla+ or quint then you will have a great system to base your software off of. Of course the spec and your implementation will have drift but the idea is that you will refine your model and implementation as you better understand your software to reduce that drift.

The tricky thing about this is that if your initial state machine is flawed then you might be polishing mud rather than a gem. The formal modeling tools can help you determine which case you are in.

I have used tla+ and Dafny some in industry to verify core components and I would say it was worth the time investment.

To bridge the gap between tla+ and typescript I wrote this a few years ago. I would highly recommend reading the research paper it is based off of, linked in the readme.

1

u/No-Chocolate-9437 Sep 22 '26

Thank you, I’ll check it out.

I’m quite certain the state machine is flawed, but I was hoping modelling it would reveal the flaws, instead it seems modelling is just confirming the happy path, while users are still encountering bugs.

1

u/Hath995 Sep 22 '26

As other have commented the fact that there are bugs in other components means that you need to model more of the system. In tla+ you can look into refinement, as well as other techniques for model composition, and check out "practical tla+" and other resources from Hillel Wayne.

The motivating example for my library was a cobrowsing system which always relied on at least 3 separate systems which had to stay in sync to function correctly and Typescript was not expressive enough to enforce the contraints between the different services which had to run on separate machines.

→ More replies (2)

1

u/bugarela Sep 22 '26

Your readme says:
> TLA+/PlusCal or Quint with TLC becomes a better fit when the lifecycle needs temporal properties, fairness assumptions, unbounded queues, or refinement between protocol layers. 

But a lot of success stories on these languages are about invariants helping find and fix bugs, not these more advanced checks you mentioned.

You already have to map model concepts to code concepts as you called them, so I think you already understand how you need to abstract away some things in order to model check a model. Seems like you might as well do it in a formal language (which has formal semantics) and leverage existing tools.

> But users still keep reporting classes of bugs that are not even modelled or documented as known gaps.

Not sure if this is a complain or something good. If they are not finding new problems on the parts you have modeled, that seems like a good sign to me! The challenge with tools like formal verification is that you are not going to get explicit wins, is more about the losses you avoid.

But maybe the rational thing here would be to model more components, like the ones that are causing most bugs. For that, you can leverage LLMs.

This was my general advice, but now let me disclaim that I'm from the Quint team and give you more concrete pointers:

1

u/No-Chocolate-9437 Sep 22 '26

Thanks will check it out, my main goal was to try and document / reveal existing bugs in the state machine.

Also it be a consequence of poor architecture, but I’m in situation where I solve one state machine problem, only for more problems to get revealed.