Imagine you're testing a Rust library like a shared queue or a lock — something that multiple threads hammer on at the same time. The bugs you're hunting aren't the obvious ones. They're the weird races that only happen when Thread A grabs a resource half a microsecond before Thread B does something that assumes Thread A hadn't yet. Writing tests for this kind of thing by hand is miserable, and if you get the setup wrong, your "concurrent test" is really just two threads politely taking turns.

Naturally, people have tried pointing large language models at the problem. Ask ChatGPT to generate a Rust test for a concurrent API and it'll happily produce something that compiles. The trouble is what it produces is usually one of three things: shallow (just calls the function once and checks it didn't crash), invalid (violates the API's rules — like calling unlock on something that wasn't locked), or fake-concurrent (spawns threads but they don't actually race against each other).

On the other side of the aisle, formal methods folks have been building model-based testing tools for decades. These tools genuinely understand resource ownership and state transitions, and they can systematically explore nasty interleavings. But they demand enormous amounts of hand-written glue code to turn their abstract models into tests that actually run.

This paper marries the two approaches. The insight is to use a Petri net — a classic formal model that's genuinely good at describing how resources flow through a concurrent system, forking and joining and being consumed — as a scaffold that guides the LLM. The Petri net encodes the API's real preconditions and its ownership lifecycle. The LLM handles what it's actually good at: turning abstract steps into idiomatic, compilable Rust code.

So the workflow becomes something like:

• Build a Petri net that captures the API's resource ownership rules and legal state transitions
• Use the net to generate abstract test scenarios that are guaranteed to respect preconditions and to contain genuine concurrent interleavings
• Hand those scenarios to the LLM, which fills in the actual Rust syntax, thread spawning, and assertions

The result is tests that are both semantically valid (they don't misuse the API) and behaviorally deep (they actually stress the concurrent behavior). It's a nice example of a broader pattern that's emerging: don't ask LLMs to do the reasoning part — give them a formal skeleton and let them handle translation.