Specifying a multimodal AI orchestrator in TLA+ before implementation

[Petru Mirzenco]

Hi everyone,

We wanted to share a recent production use case applying TLA+ to the domain of AI orchestration. We built a multimodal AI orchestrator by first specifying the architecture, and then writing the code to align with the spec before deploying to Google Cloud.

We built a system that generates multimodal content based on user context and private uploaded images, and conducts related searches across internal databases and the web. This requires coordinating multiple external AI services (Vision, LLM, Image/Video Generation, and Search). The underlying AI models are inherently non-deterministic and suffer from unpredictable latency spikes. If a video generation node times out, or a search API returns a malformed payload, it can trigger asynchronous race conditions, retry loops, and partially complete states where a user is billed for an asset that never delivers.

Standard integration testing couldn’t adequately cover the state space created by these asynchronous intersections.

We modeled the orchestration kernel in TLA+. We didn’t model the AI model logic itself; instead, we considered the AI agents as non-deterministic nodes that could return any value from a set of defined outcomes (e.g., Success, Timeout).

This let us verify exactly how our orchestrator would handle the AI’s unpredictable behavior before the implementation phase even began.

We wrote two separate specifications: one for the backend orchestration kernel (~58,000 states explored) and one for the frontend lifecycle (~30,000 states explored) - to make sure the user journey is consistent across environments.

The model checker identified several critical logic flaws that would not have surfaced until production:

• Retry Race Condition: A video generation task was incorrectly being reset to Idle, which immediately triggered a duplicate retry while the original task was still running.
• Configuration Boundary Bug: We tested the boundary of a MaxVideoRetries setting. One or two retries were stable, but expanding to three caused a silent failure of the Video Api — the UI loaded successfully, but the final video asset was dropped. The user would have been billed for an undelivered item.
• Data Isolation Violation: We caught a sequence where the internal storage identifiers could leak into the external AI model context payload. 

After three months deployed on GCP, we’ve had zero logic failures or state-tracking errors. Zero logic failures or state-tracking errors. During one live incident, a misconfigured secondary search service went down — the verified architecture bypassed it and delivered the primary result without system failure.

TLC Checking stats

A privacy invariant snippet

We welcome questions and feedback.

[Markus Kuppe]

Hi Petru,

thanks for sharing your success story. It will hopefully inspire others to publicly share their experiences as well.

The answer is probably no, but is your spec publicly available?

Thanks,
Markus

> TLC Checking stats<tlaproj-states-3retries.png>
>
>
> A privacy invariant snippet<tlaproj-privacy-invariant.png>

[Petru Mirzenco]

Hi Markus,

The spec isn't publicly available at the moment. We are considering sharing more modeling details in future posts. 

We also have a technical write-up covering the architecture and the verification approach. Happy to send it directly if you're interested.

Thanks,

Petru 

[Younes]

Hi Petru,

thank you for sharing, this is very interesting. I'd like to read your write-up actually if it's published.

[Petru Mirzenco]

Thank you for all who had interest. I sent the writing through private messaging.

Adding some more details and clarifications.

- While the system seemed simple (DAG with retries),  it was prone to many issues in production that hardly can be discovered during pre-launch tests. 

- To make it a reliable AI system and prevent sudden and unexplained crashes, we decided to specify it in TLA+.

- The specifications were written in pure TLA by a human systems architect.

- All safety and liveness properties have been thought and rethought by the architect and the team.

- AI assistance has been used for project research, requirements analysis, drafting the initial specs, speeding the spec updates.

- The completed specs (blueprint) were implemented with the help of AI coding agents that produced very accurate code, even following the specified security patterns (verified vibe code or vericode?).

- We did not specify anything about the AI models, but rather the allowed pathways, handoffs, spawns, failure modes, communication limits and restrictions, expected results.  

One of the readers mentioned that the orchestrator is similar to Durable Execution from Temporal/ResonateHQ. 

The goal is similar - preventing wrong AI outputs. As I understand, our system architecture is durable by design, whereas the former one checks the durability at the implementation phase.

Another question was how did we achieve determinism. 

In our system the orchestration of requests and data is deterministic. We aimed to have a stable behavior of the system no matter the input or subcomponent crash.

So, if the user provides a wrong input or a sub-model crashes, the system still has to deliver a response be it success, error or partial output. 

One more thing about the number of explored states. I was told 57k is small comparing to n*million or m*billion of real big systems. 

It all depends on the scale. We do have other specs with more than 500k states. However, this system is small but the amount of explored states is still huge. A small team, even with AI assistance can generate 2k-3k tests at most and they are still left guessing what would happen in production.

I hope the community finds the above information useful. I think TLA+ is very useful and relevant in the age of AI.

Thank you,

Petru