OpenHands、ランタイム API の競合状態を Quint で検証し修正

On-call engineers on the OpenHands team had long been plagued by a noisy "multiple valid pods" alert due to a race condition in the Runtime API. The Runtime API is an internal service within OpenHands that orchestrates execution sandboxes for our coding agents. The race condition caused duplicate Kubernetes pods to spin up for the same conversation runtime. We used DataDog logs to investigate the situation, drafted fixes, and eventually used Quint to check whether those fixes would actually solve the problem. Quint's model of the Runtime API proved critical, catching an incomplete fix in a version of the software. Indeed we observed the bug of the “fixed” version in production, as predicted by Quint. Before shipping the next version, we used Quint to check the next fix to arrive at a solution we could be confident in. As of May 5, 2026, the multiple valid pods alert is gone, ending a longstanding source of alert fatigue. In this post, we walk you through how we diagnosed the race condition, why our initial fixes fell short, and how Quint gave us the confidence to ship a solution that fixes the issue.

Waiting Out the Alert

As an on-call engineer on the OpenHands team, one of our noisiest alerts has been "multiple valid pods". In Kubernetes, a pod is a running instance of a service, and in this case, each conversation runtime gets its own pod. When this alert fired, it would show up in waves. The suggested action on the alert is to find duplicate Kubernetes pods for an OpenHands conversation runtime and delete one pod. However, it feels risky to delete pods in production manually. What if we negatively impact the conversation experience for an active logged in user? Eventually, the alerts would quiet down on their own, so I and other on-call engineers would opt to wait out the alert. Unfortunately, having unactionable alerts is not a good sign. It reduces confidence in our alerting and instead increases alert fatigue. However, this issue seemed to be a hard one to solve as multiple people had unsuccessfully tried to fix this bug before.

OpenHands Finds a Race Condition

We decided to investigate the cause once more. As the first step, I had the OpenHands agent look at DataDog logs to investigate the alert. It reported a race condition as follows.

I then had the OpenHands agent draft up a fix: check for existing active pods in the resume function before scaling up in our Runtime API (a custom Kubernetes controller).

The problem, however, was that I did not have confidence in the fix. Runtime API is a black box to most of us here on the OpenHands team with only a select few truly understanding how it works.

Enter Quint

Quint is a specification language that models distributed systems and a set of tools that apply different formal methods to them. Quint can prove that properties hold across the various states your system can be in. Why is this important? A race condition is a bad state your system can get into. Quint can model your system and also unmerged code changes to prove that your system can no longer get into that bad state with those changes.

What is the Quint LLM Kit?

Quint LLM Kit packages Claude Code with Quint tools into a container. It is an easy-to-use Quint setup.

Fortunately, our chief architect Ray Myers had already used the Quint llm-kit to model the Runtime API with Quint and shared the spec files with me.

An incomplete fix and Quint’s prediction

As I didn’t have confidence in the fix proposed by the agent, I decided to investigate the issue using the existing Quint model: I started an agent with Quint LLM Kit and pointed the setup at the Runtime API repository on my local machine. I asked the agent if it could see the Quint spec files. Before merging the OpenHands agent fix to check for existing active pods before resume, I told Quint about the race condition and the pull request with the fix. Before updating its existing model of the Runtime API, Quint tried to find the race condition. It found the race condition quickly. Race conditions are notoriously tricky as they are difficult to understand and reproduce, so it was neat to have a tool like Quint teach me how the Runtime API worked via its modelling which also presented a way to reason about the race condition.

Next, Quint updated its model and told us that the fix was incomplete. That there would still exist some variation of the race condition.

Specifically it called out an edge case with terminating pods. Interestingly, in our OpenHands agent fix, there was an exclude filter for terminating pods or pods with a deletion timestamp.

At this point, I decided to not investigate this any further. I put the fix in as-is because it felt like it would already be better than the status quo (the noisy alerts that we have already been dealing with for a very long time). I hoped the race condition was resolved.

Finding a real fix and confirming it with Quint

As you might have guessed, I continued to see the multiple valid pods alert. This meant that the race condition was still around. I asked the OpenHands agent to investigate DataDog logs again and to check if this was the same issue that the merged PR tried to fix.

The OpenHands agent analysis shows the merged PR fix incorrectly filtered out terminating pods. Prior Quint analysis had already mentioned the fix was an incomplete fix and included a snippet about the case around terminating pods. At this point in time, the resume functionality in the Runtime API did not see terminating pods as active pods and created new duplicate pods. The OpenHands agent created a new PR fix to remove the one line filter of the terminating pods.

I asked Quint if the new PR fix would fully close the race condition. It told me no.

While the Runtime API would now count terminating pods as active, it still instructed Kubernetes to maintain spec_replicas=1. Kubernetes, when working toward that target, ignores terminating pods. As a result it sees zero active pods and spins up a new one, creating a duplicate. Seeing that the new PR fix would not fully close the race condition according to Quint, I closed the PR.

I then asked the Quint llm-kit for a solution that would fully close the race condition. Quint came up with a solution that incorporates the one line closed PR fix to view terminating pods as active pods and also waits until terminating pods are gone before scaling up.

The combination of the initial merged fix and the latest solution that Quint came up with is the only one where the noDuplicatePods property holds in Quint’s model of the Runtime API as is shown by the following table.

This analysis gave us more confidence in the latest solution. I got it merged.

Current situation

After merging the fix, we planned out the next steps. The plan is that I would observe if we get any more Multiple Valid Pods alerts. If so, I would ask the OpenHands agent to analyze DataDog logs and if this was the same race condition that the latest PR fix tried to address. If yes, we would need to update the Quint model further to come up with a solution that accurately reflects the Runtime API. If not, it could mean the race condition is closed. Or it could mean there are other race conditions that are not visible in the Quint model (potentially because the model is too simplistic).

However, I’m happy to report that we no longer see the Multiple Valid Pods alert as of today. This longstanding issue that multiple people have tried to fix many times is finally solved.

Conclusions

Without Quint, we would have shipped a fix, watched the alerts continue, and never known why. Quint gave us something rare in distributed systems debugging: a way to reason about correctness before committing to production.

If you're dealing with noisy alerts you can't confidently act on, that's often a sign of a system that's hard to reason about. Quint and the llm-kit doesn't just tell you your fix is wrong. It helps you find one you can trust. Seeing the successful predictions changed my point of view; I’m a believer in formal methods now.

“In 77 years since Turing first did program proofs on paper, we've finally made it practical.” — Ray Myers