LLM Output Not Flushed to File Before MCP Execution in GenAIScript

[lemmy]

When running the following script, it appears that GenAIScript does not serialize the LLM's output (i.e., the generated specification) to the output file before invoking the MCP server. As a result, the MCP receives no input, and the MCP process fails to execute as expected.

script({
    files: "puzzles/SomePuzzle.md"
})

defTool({
    tla: {
        url: "http://localhost:59071/mcp",
        type: "http"
    }
})

const file = env.files[0];
const baseName = file.filename.replace(/\.[^.]*$/, '');
const fileName = baseName.split('/').pop();
defFileOutput(fileName + ".tla", "the created TLA+ specification")

$`Formalize the puzzle ${file.filename} using TLA+: Create a TLA+ specification that captures the problem's requirements and constraints. Use the TLC model checker via the tla_tlaplus_mcp_sany_parse to parse the specification. If parsing fails, you will need to fix the specification and try again.`

Json schema of this particular MCP server, formalizing that the MCP requires a fully-qualified filename as input:

  {
    "name": "tlaplus_mcp_sany_parse",
    "description": "Parse the input TLA+ module using SANY from the TLA+ tools. Use SANY to perform syntax and level-checking of the module. Ensure that the input is provided as a fully qualified file path, as required by the tool.",
    "inputSchema": {
      "type": "object",
      "properties": {
        "fileName": {
          "type": "string",
          "description": "The full path to the file containing the TLA+ module."
        }
      },
      "required": [
        "fileName"
      ],
      "additionalProperties": false,
      "$schema": "http://json-schema.org/draft-07/schema#"
    }
  },

The expected behavior is for the generated .tla file (containing the TLA+ specification) to be written before the MCP server gets invoked. How can we force GenAIScript to flush or persist the LLM's output to the/a target file before invoking the MCP tool?

[lemmy]

Below is an even simpler example. As you can see, the MCP call fails because the file doesn't exist at that time.

defTool({
    tla: {
        url: "http://localhost:59071/mcp",
        type: "http"
    }
})


$`Create a simple TLA+ spec, write it to a file, and parse it.`
defFileOutput("SimpleSpec.tla", "TLA+ spec")

-> % genaiscript run tlatranslate -y
genaiscript: tlatranslate
trace: /Users/markus/src/TLA/_specs/RiverCrossingWithAFlashlight/.genaiscript/runs/tlatranslate/2025-07-31T23-10-47-328Z-_38wE6kiOka3-a1NifLnH/trace.md
output: /Users/markus/src/TLA/_specs/RiverCrossingWithAFlashlight/.genaiscript/runs/tlatranslate/2025-07-31T23-10-47-328Z-_38wE6kiOka3-a1NifLnH/readme.md
gh auth token
mcp: starting tla
mcp tla: tools: /Users/markus/src/TLA/_specs/RiverCrossingWithAFlashlight/.genaiscript/mcp/tla/tools/7527401a7db2a0f649d42c6ab209643b483ac8d49aada5d25cb4e45f75068c37.json
mcp tla: tools sha: 53749e97390f87d705cee839f4890a322732f7cac58d4aac2199efd7495dfffe
gh auth token
╭─💬 github:openai/gpt-4.1 ✉ 2 
├─🔧 tools (5)
│ tla_tlaplus_mcp_sany_parse, tla_tlaplus_mcp_sany_symbol, tla_tlaplus_mcp_tlc_check, tla_tlaplus_mcp_tlc_smoke, tla_tlaplus_mcp_tlc_explore
╭─📙 system
│## Safety: Jailbreak
│... (60 lines)
│When generating files, use the following rules which are formatted as "file glob: descr…
│   SimpleSpec.tla: TLA+ spec
╭─👤 user
│Create a simple TLA+ spec, write it to a file, and parse it.


╰─🏁  github:openai/gpt-4.1 ✉ 2 1100ms ⇅ 1.4kt ↑1.4kt ↓27t 0.305¢
╭─💬 github:openai/gpt-4.1 ✉ 4 
├─🔧 tools (5)
│ tla_tlaplus_mcp_sany_parse, tla_tlaplus_mcp_sany_symbol, tla_tlaplus_mcp_tlc_check, tla_tlaplus_mcp_tlc_smoke, tla_tlaplus_mcp_tlc_explore
╭─📙 system
│## Safety: Jailbreak
│... (60 lines)
│When generating files, use the following rules which are formatted as "file glob: descr…
│   SimpleSpec.tla: TLA+ spec
╭─👤 user
│Create a simple TLA+ spec, write it to a file, and parse it.
╭─🤖 assistant 
├──📠 tool tla_tlaplus_mcp_sany_parse (call_bcEYYBgSRhXGocyZktJRdrAx)
│ {"fileName":"SimpleSpec.tla"}
╭─🔧 tool call_bcEYYBgSRhXGocyZktJRdrAx
│File /Users/markus/src/TLA/_specs/RiverCrossingWithAFlashlight/SimpleSpec.tla does not …


File SimpleSpec.tla:
`tla
---- MODULE SimpleSpec ----
VARIABLES x

Init == x = 0

Next == x' = x + 1

Spec == Init /\ [][Next]_x

==== 
`

This is a simple TLA+ specification that describes a variable x, initialized to 0, which can increase by 1 in each step.

╰─🏁  github:openai/gpt-4.1 ✉ 4 1448ms ⇅ 1.6kt ↑1.5kt ↓84t 0.366¢
updating SimpleSpec.tla
genaiscript: success
> 2548ms ↑2.9kt ↓111t 1186.48t/s 0.671¢
  github:gpt-4.1-2025-04-14> 2548ms ↑2.9kt ↓111t 1186.48t/s 0.671¢
    ✉ 2, 1.4kt, 0.305¢
    ✉ 4, 1.6kt, 0.366¢
   trace: /Users/markus/src/TLA/_specs/RiverCrossingWithAFlashlight/.genaiscript/runs/tlatranslate/2025-07-31T23-10-47-328Z-_38wE6kiOka3-a1NifLnH/trace.md
  output: /Users/markus/src/TLA/_specs/RiverCrossingWithAFlashlight/.genaiscript/runs/tlatranslate/2025-07-31T23-10-47-328Z-_38wE6kiOka3-a1NifLnH/readme.md

[pelikhan]

I see, files are not written until the end of the chat which happens way after we invoke MCPs. We would probably need to add a tool (mcp or not) that can write file so that these sequence happens in order.

• Can you mod your MCP to take the .tla source instead?
• how do I repro?

[lemmy]

Thanks for your response. I suppose I could modify my MCP server to accept not just a file name, but also raw file content as input. The MCP server could then serialize the content to a temporary file before passing it along to the CLI tool that the MCP wraps.

However, I see two main drawbacks to this approach:
a) It would make the MCP API more complex, which could be confusing for AI systems interacting with it.
b) I’d need to implement this serialization logic in every MCP I create, which adds extra overhead.

In general, many CLI tools, or legacy tools in general, expect file inputs. It would be ideal to support this natively, especially considering that tools like Cursor and GitHub Copilot don't require this kind of serialization step.

You can reproduce the issue by installing the TLA+ VSCode extension in Cursor (ext id: tlaplus.vscode-ide), activating the TLA+ MCP server once, and using the scripts I mentioned above.

[lemmy]

Additionally, when working with files, there's the added challenge of enabling the LLM to operate on the modified files after the MCP has been invoked. Another challenge with files arises if the MCP is running remotely.

[pelikhan]

one thing we can do here is do an inline prompt, take the result and apply it to the files, then execute the MCP tool directly.

[lemmy]

Wouldn't that design shift the decision to use an MCP server from the AI back to the human authoring the GenAIScript?

[pelikhan]

Yes completely.

To support the scenario you want, we would need to add a tool that can write a files. The LLM will (likely) call that tool then call TLA+.

[lemmy]

It seems that LLMs are able to correctly use my MCP tools when a fs_write_file tool is included in the setup.

defTool(
    "fs_write_file",
    "Writes text to a file in the file system. Use this to create or update files in the workspace before using the TLA+ MCP tools.",
    {
        filename: { type: "string" },
        content: { type: "string" },
    },
    async ({ filename, content }) => {
        await workspace.writeText(filename, content);
        return { success: true, filename };
    }
)

Can I assume that workspace.writeText includes basic security safeguards. For example, preventing writes to paths outside the GenAIScript workspace? Also, would it make sense to include fs_write_file as a system tool?

[lemmy]

By the way, I receive the following notification for each of my issue comments:

https://github.com/microsoft/genaiscript/actions/runs/16727798214

[lemmy]

Can I assume that workspace.writeText includes basic security safeguards. For example, preventing writes to paths outside the GenAIScript workspace?

No, this is not the case. The LLM managed to generate files in the /tmp directory, which is outside the VSCode workspace.

[pelikhan]

This release https://github.com/microsoft/genaiscript/releases/tag/2.3.14 introduced a new function "fs_write_file" and also systematic runtime check in the runtime write apis.