Feature request: first-class TLA+ / TLC (Java) runtime support

## Summary

Add first-class **TLA+ / TLC (and PlusCal/SANY)** support to `ado-aw` so agentic workflows can run **formal model checking** of state machines and protocols. Today `runtimes:` covers `lean`, `python`, `node`, and `dotnet`, but there is no Java/TLA+ runtime — so a workflow that wants to model-check a spec has to hand-roll the toolchain in `steps:` and manually widen the network allowlist.

This is a natural companion to the existing `runtimes: lean` (theorem proving): **TLC complements Lean** — TLA+/TLC is the right tool for *discovering* liveness/safety gaps (it exhaustively searches and emits counterexample traces), while Lean *proves* a fixed design. Agentic "find stuck-state / deadlock / missing-timeout bugs in this state machine" workflows want TLC.

## Motivation / use case

We want a scheduled agentic workflow that scans a codebase for event-driven state machines, builds **TLA+** models, and runs **TLC** to find liveness gaps (states that can wedge forever) — then proposes the models + findings via safe-outputs (draft PR + work item per gap). This is fully within the agentic-workflow sweet spot, but the toolchain is currently DIY.

## What's missing

TLC is a Java application distributed as a single `tla2tools.jar` (includes TLC, the SANY parser, and the PlusCal translator). To run it in a sandboxed AWF agent you need:

1. **A JRE/JDK** — no Java runtime exists in `ado-aw` today.
2. **`tla2tools.jar`** — fetched/cached (latest from the TLA+ releases, or a pinned version).
3. **Network allowlist entries** for the download sources (e.g. a JRE provider such as Adoptium/Temurin, and the GitHub release asset for `tla2tools.jar`). GitHub is in the built-in allowlist; the JRE provider domain is not.
4. **bash allow-list extension** so the agent may invoke the toolchain (e.g. `java`, plus convenience wrappers like `tlc` / `pluscal` / `sany`, and `tar`/`curl` for provisioning) — analogous to how `runtimes: lean` auto-adds `lean`/`lake`.

## Proposed solution

A first-class runtime mirroring the existing `lean` entry:

```yaml
runtimes:
tla:
version: "1.8.0" # tla2tools.jar version (optional; default latest)
jdk: "21" # JRE/JDK major (optional; sensible default)
```

When enabled it would, like other runtimes:
- install a JRE and stage `tla2tools.jar` (cached across runs),
- auto-extend the **bash allow-list** with the toolchain commands,
- auto-add the **network domains** needed to provision it (so workflow authors don't hand-maintain `network.allowed`),
- expose a stable invocation path (e.g. a `tlc`/`pluscal`/`sany` shim, or documented env vars for the `java -cp tlc2.TLC ...` form).

## Current workaround (what we have to do today)

```yaml
steps:
- bash: |
set -euo pipefail
mkdir -p "$AGENT_TEMPDIRECTORY/tla"
curl -sSL "https://api.adoptium.net/v3/binary/latest/21/ga/linux/x64/jre/hotspot/normal/eclipse?project=jdk" -o "$AGENT_TEMPDIRECTORY/tla/jre.tgz"
tar -xzf "$AGENT_TEMPDIRECTORY/tla/jre.tgz" -C "$AGENT_TEMPDIRECTORY/tla"
curl -sSL "https://github.com/tlaplus/tlaplus/releases/latest/download/tla2tools.jar" -o "$AGENT_TEMPDIRECTORY/tla/tla2tools.jar"
displayName: "Provision TLA+ toolchain (JRE + TLC)"
network:
allowed:
- "api.adoptium.net"
- "*.adoptium.net"
```
The agent then runs `java -cp tla2tools.jar tlc2.TLC -config M.cfg M.tla`. This works but every author must repeat the provisioning, pin/refresh versions by hand, and curate the allowlist — exactly the boilerplate `runtimes:` exists to remove.

## Acceptance criteria

- [ ] `runtimes: tla` (or `runtimes: tlaplus`) provisions a JRE + `tla2tools.jar`, cached across runs.
- [ ] Optional version pinning for both the JDK and `tla2tools.jar`.
- [ ] Toolchain bash commands auto-added to the allow-list.
- [ ] Required provisioning domains auto-added to the network allowlist (no manual `network.allowed`).
- [ ] A documented, stable invocation (shim or env var) for running TLC / translating PlusCal / parsing with SANY.
- [ ] Docs/example under `docs/runtimes.md` (and ideally a sample workflow) showing a TLA+ model-checking agent.

## Notes

- A general-purpose **Java/JVM runtime** would also satisfy this (TLA+ being one consumer); a thin `tla` runtime on top of it would be ideal.
- Memory: TLC benefits from a parallel GC and a decent heap; a sensible default `-XX:+UseParallelGC` and heap sizing (or a knob) would help.