[BUG] Race condition when LLM model calls prove and verify tools simultaneously

[minhanhld]

Race condition when LLM model calls scarb prove and verify tools simultaneously

Description

• When using the GPT model, there is a race condition when both prove and verify tools are called together
• Both tools operate in the same workspace and each automatically closes the workspace upon completion
• If one tool finishes before the other, it closes the shared workspace, preventing the second tool from completing successfully

Observed behavior

1. GPT model initiates both tool calls concurrently
2. First tool to finish closes the shared workspace
3. Second tool fails with workspace access errors

Expected behavior

Tools should run sequentially to prevent workspace conflicts, or workspace closing should be coordinated

Possible causes

The agent's parallel tool calling capability conflicts with the workspace management design where each tool independently closes the workspace

Suggested fixes

1. Modify the agent prompt to ensure sequential tool calls rather than parallel
2. Implement a locking mechanism for the workspace (mutex ?)
3. Only close the workspace when all tools using it have completed

Priority

Low - This should only happen if a user wants to prove AND verify in the same query, but things should still work if those tools are called separately.