feat(runtimes): add first-class TLA+/TLC runtime support

docs/runtimes.md

@@ -165,6 +165,99 @@ When enabled, the compiler:
 - **`config:` is functional, not a deferred warning.** AWF only overlays files in `$HOME` (e.g., `~/.npmrc` → `/dev/null`); workspace files such as `nuget.config` are preserved inside the agent sandbox, so a checked-in `nuget.config` works today.
 - **`NuGetAuthenticate@1` requires no `workingFile:` input.** It auto-discovers `nuget.config` files anywhere in the workspace, unlike `npmAuthenticate@0` which needs an explicit path.
 
+### TLA+ (`tla:`)
+
+TLA+ / TLC formal model-checking runtime. Uses `JavaToolInstaller@0` to select a pre-installed JDK and downloads `tla2tools.jar` from the TLA+ GitHub releases page, then creates convenience shims (`tlc`, `pluscal`, `sany`) and extends the bash command allow-list.
+
+TLA+ is a natural complement to the `lean` runtime: **TLC discovers** liveness/safety gaps by exhaustively searching the state space and emitting counterexample traces, while **Lean proves** a fixed design. Agentic workflows that scan codebases for state-machine bugs — finding stuck states, deadlocks, and missing timeouts — are a primary use case.
+
+```yaml
+# Simple enablement (latest tla2tools.jar, JDK 21 LTS)
+runtimes:
+  tla: true
+
+# With options (pin tla2tools.jar and JDK versions)
+runtimes:
+  tla:
+    version: "1.8.0"   # tla2tools.jar version (omit for latest)
+    jdk: "21"          # JDK major version (default: 21)
+```
+
+**Fields:**
+
+| Field | Type | Description |
+|-------|------|-------------|
+| `version` | string | `tla2tools.jar` version to download from the TLA+ GitHub releases (e.g., `"1.8.0"`, `"1.7.3"`). When omitted, the latest release is downloaded via GitHub's `releases/latest/download/` redirect. |
+| `jdk` | string | JDK major version to pass to `JavaToolInstaller@0` (pre-installed on the build agent), e.g., `"21"`, `"17"`. Defaults to `"21"` (current LTS). |
+
+When enabled, the compiler:
+- Contributes a `JavaToolInstaller@0` task step (pre-installed mode) that selects the JDK matching `jdk:` and sets `JAVA_HOME`
+- Contributes a bash step to `Declarations::agent_prepare_steps` that:
+  1. Downloads `tla2tools.jar` from [TLA+ GitHub releases](https://github.com/tlaplus/tlaplus/releases) into `$HOME/.tla/`
+  2. Creates convenience shims (`tlc`, `pluscal`, `sany`) in `$HOME/.tla/bin/` that delegate to `java` from PATH
+- Auto-adds `java`, `tlc`, `pluscal`, `sany` to the bash command allow-list
+- GitHub is already in the built-in allowlist so no extra network host entry is needed for `tla2tools.jar`. The JDK is provided by `JavaToolInstaller@0` (pre-installed on the build agent) so no additional network access is needed for the JDK either.
+- Mounts `$HOME/.tla` and `$(JAVA_HOME)` into the AWF container via `--mount` (read-only) so the toolchain is accessible inside the agent sandbox
+- Prepends `$HOME/.tla/bin` and `$(JAVA_HOME)/bin` to `PATH` inside the AWF sandbox
+- Sets `TLA_JAR` as a pipeline variable so downstream steps can reference the jar path
+- Appends a prompt supplement informing the agent about TLA+ availability and invocation patterns
+
+**Shims:**
+
+| Command | Java main class | Description |
+|---------|----------------|-------------|
+| `tlc` | `tlc2.TLC` | Run the TLC model checker: `tlc -config M.cfg M.tla` |
+| `pluscal` | `pcal.trans` | Translate PlusCal to TLA+: `pluscal -nocfg M.tla` |
+| `sany` | `tla2sany.SANY` | Parse and syntax-check a spec: `sany M.tla` |
+
+You can also invoke the JVM directly: `java -XX:+UseParallelGC -cp "$TLA_JAR" tlc2.TLC -workers auto -config M.cfg M.tla`
+
+**Environment variables available inside the agent sandbox:**
+
+| Variable | Value |
+|----------|-------|
+| `TLA_JAR` | Absolute path to `tla2tools.jar` |
+| `JAVA_HOME` | JDK home directory (set by `JavaToolInstaller@0`) |
+
+**Example: TLA+ model-checking workflow**
+
+```yaml
+---
+name: tla-liveness-checker
+description: |
+  Scans the codebase for event-driven state machines, builds TLA+ models,
+  runs TLC to find liveness gaps, and proposes findings via safe-outputs.
+on:
+  schedule: "weekly on monday"
+runtimes:
+  tla: true
+tools:
+  bash:
+    - find
+    - grep
+    - tlc
+    - pluscal
+    - sany
+    - java
+safe-outputs:
+  create-pull-request: {}
+  create-work-item: {}
+---
+
+Scan the repository for state machine implementations (look for enums with
+state names, switch/match blocks on state, or explicit state transition maps).
+
+For each state machine found:
+1. Build a TLA+ model in a temp file capturing the states and transitions.
+2. Run `pluscal` to translate PlusCal if used, or write TLA+ directly.
+3. Run `tlc -config <cfg> <spec>.tla` to check for deadlocks and liveness.
+4. If TLC finds a counterexample trace, record the violation.
+
+If violations are found, propose:
+- A draft PR adding the TLA+ models under `formal/` in the repository.
+- A work item per liveness gap with the TLC counterexample trace attached.
+```
+
 ### Combining Runtimes
 
 Multiple runtimes can be enabled simultaneously:
@@ -178,6 +271,8 @@ runtimes:
   dotnet:
     version: "8.0.x"
   lean: true
+  tla:
+    version: "1.8.0"
 ```
 
 All runtime extensions are sorted into `ExtensionPhase::Runtime` and execute before tool extensions (`ExtensionPhase::Tool`), ensuring language toolchains are available before any tools that depend on them.

prompts/create-ado-agentic-workflow.md

@@ -495,6 +495,13 @@ runtimes:
   # lean:
   #   toolchain: "leanprover/lean4:v4.29.1"   # pin a specific version
 
+# TLA+ / TLC formal model checker
+runtimes:
+  tla: true
+  # tla:
+  #   version: "1.8.0"   # pin tla2tools.jar version (omit for latest)
+  #   jdk: "21"          # JDK major version for JavaToolInstaller@0 (default: 21)
+
 # Python
 runtimes:
   python: true
@@ -529,7 +536,7 @@ runtimes:
     version: "8.0.x"
 ```
 
-> Each enabled runtime auto-adds its ecosystem's bash commands (e.g., `dotnet`, `python`, `node`, `npm`, `lean`, `lake`) and network domains to the allowlist. See `docs/runtimes.md` for full configuration reference.
+> Each enabled runtime auto-adds its ecosystem's bash commands (e.g., `dotnet`, `python`, `node`, `npm`, `lean`, `lake`, `tlc`, `java`) and network domains to the allowlist. The `tla:` runtime uses `JavaToolInstaller@0` (pre-installed JDK) and the built-in GitHub allowlist, so it requires no extra network entries. See `docs/runtimes.md` for full configuration reference.
 
 ### Step 15 — Network (standalone target only)
 
@@ -544,7 +551,7 @@ network:
     - "evil.example.com"
 ```
 
-`allowed` accepts raw domain patterns (wildcards supported) or ecosystem identifiers (`python`, `node`, `rust`, `dotnet`, `lean`) that expand to the full set of package registry domains for that ecosystem. The built-in allowlist includes: Azure DevOps, GitHub, Microsoft identity, Azure services, Application Insights, and MCP-specific endpoints for each enabled server.
+`allowed` accepts raw domain patterns (wildcards supported) or ecosystem identifiers (`python`, `node`, `rust`, `dotnet`, `lean`, `java`) that expand to the full set of package registry domains for that ecosystem. The built-in allowlist includes: Azure DevOps, GitHub, Microsoft identity, Azure services, Application Insights, and MCP-specific endpoints for each enabled server.
 
 ### Step 16 — Parameters (optional)
 

src/compile/common.rs

@@ -3224,6 +3224,7 @@ mod tests {
             python: None,
             node: None,
             dotnet: None,
+            tla: None,
         });
         let params = engine_args_for(&fm).unwrap();
         assert!(
@@ -3259,6 +3260,7 @@ mod tests {
             python: None,
             node: None,
             dotnet: None,
+            tla: None,
         });
         let params = engine_args_for(&fm).unwrap();
         assert!(

src/compile/extensions/mod.rs

@@ -571,6 +571,7 @@ pub use crate::runtimes::dotnet::DotnetExtension;
 pub use crate::runtimes::lean::LeanExtension;
 pub use crate::runtimes::node::NodeExtension;
 pub use crate::runtimes::python::PythonExtension;
+pub use crate::runtimes::tla::TlaExtension;
 pub use crate::tools::azure_devops::AzureDevOpsExtension;
 pub use crate::tools::cache_memory::CacheMemoryExtension;
 pub use ado_aw_marker::AdoAwMarkerExtension;
@@ -600,6 +601,7 @@ extension_enum! {
         Python(PythonExtension),
         Node(NodeExtension),
         Dotnet(DotnetExtension),
+        Tla(TlaExtension),
         AzureDevOps(AzureDevOpsExtension),
         CacheMemory(CacheMemoryExtension),
         AzureCli(AzureCliExtension),
@@ -742,6 +744,11 @@ pub fn collect_extensions(front_matter: &FrontMatter) -> Vec<Extension> {
     {
         extensions.push(Extension::Dotnet(DotnetExtension::new(dotnet.clone())));
     }
+    if let Some(tla) = front_matter.runtimes.as_ref().and_then(|r| r.tla.as_ref())
+        && tla.is_enabled()
+    {
+        extensions.push(Extension::Tla(TlaExtension::new(tla.clone())));
+    }
 
     // ── First-party tools (ExtensionPhase::Tool) ──
     if let Some(tools) = front_matter.tools.as_ref() {

src/compile/standalone.rs

@@ -176,6 +176,7 @@ mod tests {
             python: None,
             node: None,
             dotnet: None,
+            tla: None,
         });
         let exts = super::super::extensions::collect_extensions(&fm);
         let domains = allowed_domains(&fm, &exts).unwrap();
@@ -201,6 +202,7 @@ mod tests {
             python: None,
             node: None,
             dotnet: None,
+            tla: None,
         });
         let exts = super::super::extensions::collect_extensions(&fm);
         let domains = allowed_domains(&fm, &exts).unwrap();

src/compile/types.rs

@@ -569,6 +569,14 @@ pub struct RuntimesConfig {
     /// equivalent for selecting a package source.
     #[serde(default)]
     pub dotnet: Option<crate::runtimes::dotnet::DotnetRuntimeConfig>,
+
+    /// TLA+ / TLC formal model-checking runtime.
+    /// Downloads a JRE from Eclipse Temurin (Adoptium) and `tla2tools.jar`
+    /// from the TLA+ GitHub releases page, creates convenience shims
+    /// (`tlc`, `pluscal`, `sany`), adds Java ecosystem domains to the AWF
+    /// network allowlist, and extends the bash command allow-list.
+    #[serde(default)]
+    pub tla: Option<crate::runtimes::tla::TlaRuntimeConfig>,
 }
 
 impl SanitizeConfigTrait for RuntimesConfig {
@@ -585,6 +593,9 @@ impl SanitizeConfigTrait for RuntimesConfig {
         if let Some(ref mut dotnet) = self.dotnet {
             dotnet.sanitize_config_fields();
         }
+        if let Some(ref mut tla) = self.tla {
+            tla.sanitize_config_fields();
+        }
     }
 }
 

src/runtimes/mod.rs

@@ -13,3 +13,4 @@ pub mod dotnet;
 pub mod lean;
 pub mod node;
 pub mod python;
+pub mod tla;