AnviLTS

Build safer concurrent systems with your AI agents by giving them the ability to formally model your system and mathematically prove it free of deadlock and logic bugs

Comment

Inspiration

In College, I learnt various formal modeling tools. One of these was LTSA (labelled transition system analyzer), a formal tool that can be used to prove a concurrent system is deadlock-free and correct against safety and liveness properties. That usecase is obviously really beneficial but being a academic tool, LTSA is not very accessible to engineers in industry. Thankfully though, with LLMs now becoming a daily part of coding, they don't need to anymore. What if each engineer could have a formal modeling expert that they can direct to their code, and get safety guarantees on. That's what I'm hoping to achieve.

Background

Concurrency bugs are an incredible PITA: deadlocks and race conditions surface in extremely rare and obscure scenarios but are very disruptive when they do (and always in production). These days though we write concurrent systems with AI agents like Codex and while they are good at writing concurrent code, reasoning about that code is a different matter. No amount of tool use and execution lets an LLM exhaustively explore every interleaving of a running system (not without burning through a ton of tokens anyway). This is a combinatorial problem and its already solved in the world of formal methods. A tool like LTSA was built specifically for this.

The catch though is that its locked behind steep formal notations (FSP) which few people in industry know, are typically not that well documented and whose studying tends to be a research exercise. The notations also make them inaccessible to AI agents. FSP is as mentioned earlier not that well documented, so often LLMs will write faulty notations that aren't accepted by the tool. But the underlying engine of LTSA is where the actual value sits, and that engine is driven by state machines and programmable logic. The formal notations were (ironically) only there to provide simpler access to the underlying engine. If we just made the engine available to an agent via an MCP server for example, it wouldn't need to know any formal language, it just needs to use a tool. Now suddenly, our agents have the ability to model concurrent systems as they write it (or even model existing concurrent systems), and then verify these systems are correct. A gamechanging advancement.

AnviLTS

AnviLTS is a model checker that plugs into Codex over MCP. Codex turns your concurrent code into a Labelled Transition System (which is just a state machine really), and invokes AnviLTS to mathematically prove the following properties on the composed system:

  • Deadlock freedom: Is there a reachable state where the whole system gets stuck?
  • Safety: "nothing bad ever happens" (mutual exclusion, no illegal orderings).
  • Liveness/progress: "something good eventually happens" (no request is starved forever).

When a property fails, it returns a counterexample: the exact sequence of actions (and, for liveness, the infinite cycle) that breaks it, rendered as a highlighted state-graph (at the user's request). The agent then fixes the code and re-verifies.

There are four tools to interact with the engine provided via the MCP server:

  1. validate_model
  2. compose_lts
  3. verify_lts
  4. render_lts

How it's built

The official LTSA tool only accepts FSP as an input, so that was off the table. I've worked on LTSA in the past and even setup a localized VSCode extension for it. As such, having an understanding of how the tool's core logic works, I instead decided to work with codex to reconstruct the core engine of LTSA from scratch (using the actual LTSA tool for parity checking). The reconstruction was done in TypeScript and as of present, the reconstructed engine can perform all the core functions of LTSA (process composition, deadlock detection, safety and liveness checking).

I validated the reconstructed engine against the official engine via differential testing. The LTSA textbook includes many examples that can be effective testcases to check parity against, so I setup a harness that runs the official LTSA tool on them, and then converted the output into a set of testcase results that AnviLTS would have to match (AnviLTS doesn't ingest FSP like LTSA, so I had to convert the examples in the textbook to state machine jsons). Running the engine through the test matched on all 62 test cases (44 deadlock 8 safety and 10 liveness).

The next step was encasing this engine in an MCP server so an agent can utilize it. I added specific instructions in the MCP server to enquire with the user if the model its defining is an accurate representation of the system, and only on the user's approval, do the verification. This human-in-the-loop step is critical since the agent won't always have context on the system as a whole, so the human can fill in this gap. To do this though, it's vital the user has clear observability on how the agent is modeling their system, so each transition in the model has attached a code citation which points to the specific location in code that transition is representing.

Each agent also carries an abstraction ledger recording assumptions, omissions, unresolved questions, and the source revision it was built against. This evidence survives composition, so when AnviLTS hands back a counterexample, every step in that trace points straight back to the code it came from (or is clearly flagged as an assumption). All this impresses on the necessary involvement of the individual, the agent isn't claiming that its model perfectly matches the source code, that is for the user given all necessary details via code provenance to validate, and only once validated, will AnviLTS prove safety under those stated assumptions.

Challenges I ran into

  • State-space explosion on larger models. The official LTSA tool does a number of tricks to avoid or reduce likelihood of this, I had to largely rely on just only exploring the reachable space which tends to be more reasonable
  • Making sure the agent properly models the system. Agents don't have complete context on your system so I mitigated this by requiring user review and presenting code provenance
  • Visualization for traces was unusually slow in Codex, and I wanted to see what optimizations I could do but I honestly didn't have the time.

What's next

Visualization optimizations, State explosion optimizations, and some more features that LTSA has ported over. Also I'm interested in building bridges to other formal tools: Alloy, TLA+, SAT Solvers etc. These all have the potential to be really useful in a lot of industry cases but are not that widely used as of now.

Built With

Share this project:

Updates