feat: add Lean 4 runtime support with runtimes: front matter (#208)

* feat: add Lean 4 as a first-class tool

Add `tools: lean:` front matter configuration that auto-configures:
- elan installation step (injected into prepare_steps before AWF sandbox)
- lean/lake/elan added to bash command allow-list
- Lean-specific domains (elan.lean-lang.org, leanprover.github.io,
  lean-lang.org) added to AWF network allowlist
- Agent prompt supplement informing the agent Lean 4 is available

Supports both simple (`lean: true`) and object (`lean: { toolchain: ... }`)
front matter formats. Default toolchain is "stable"; lean-toolchain files
in the repo override automatically via elan.

Includes:
- LeanToolConfig types with deserialization tests
- Lean domain entries in allowed_hosts.rs
- Standalone compiler wiring (prepare_steps, allowed_domains, copilot_params)
- 1ES compiler: bash allow-list works; elan install via manual steps
- AGENTS.md documentation
- Example agent (examples/lean-verifier.md)
- Unit tests for types, copilot params, allowed domains, prepare steps

Related issues:
- #206 (first-class tool documentation pattern)
- #207 (network ecosystem identifiers)

Co-authored-by: Copilot <223556219+Copilot@users.noreply.github.com>

* fix: symlink lean tools into /tmp/awf-tools/ for AWF chroot compatibility

AWF chroot mode reconstructs PATH from standard system locations,
so $HOME/.elan/bin is not on PATH inside the sandbox. Symlink
lean, lake, and elan into /tmp/awf-tools/ which is always mounted
at /tmp inside the AWF container.

Co-authored-by: Copilot <223556219+Copilot@users.noreply.github.com>

* refactor: move Lean from tools to runtimes

Lean is a language runtime, not a tool (like edit, bash, memory).
Refactor to align with gh-aw's `runtimes:` front matter model:

- New `src/runtimes/` module alongside `src/tools/` and `src/safeoutputs/`
- `src/runtimes/lean.rs`: LeanRuntimeConfig, LeanOptions, install/prompt generators
- `src/runtimes/mod.rs`: module documentation
- `RuntimesConfig` struct in types.rs with `runtimes` field on FrontMatter
- Front matter changes from `tools: lean:` to `runtimes: lean:`
- All compiler references updated (standalone.rs, common.rs)
- AGENTS.md: new "Runtimes Configuration" section, separate from Tools
- Example updated

Co-authored-by: Copilot <223556219+Copilot@users.noreply.github.com>

* refactor: clean up generate_lean_install string formatting

Replace \x20 hex escape sequences with a readable approach: build
the script body as a plain string, then indent each line by 4 spaces
for the YAML block scalar.

Co-authored-by: Copilot <223556219+Copilot@users.noreply.github.com>

* fix: use lean.rs constants instead of mcp_required_hosts

- Use LEAN_BASH_COMMANDS constant in common.rs instead of inline list
- Move lean domains from mcp_required_hosts() to LEAN_REQUIRED_HOSTS
  constant in runtimes/lean.rs (lean is a runtime, not an MCP)
- Update standalone.rs and allowed_hosts.rs tests accordingly

Co-authored-by: Copilot <223556219+Copilot@users.noreply.github.com>

---------

Co-authored-by: Copilot <223556219+Copilot@users.noreply.github.com>
Co-authored-by: copilot-swe-agent[bot] <198982749+Copilot@users.noreply.github.com>

Author: 3 people

AGENTS.md

@@ -146,6 +146,10 @@ tools:                         # optional tool configuration
   #   toolsets: [repos, wit]
   #   allowed: [wit_get_work_item]
   #   org: myorg
+runtimes:                      # optional runtime configuration (language environments)
+  lean: true                   # Lean 4 theorem prover (see Runtimes section)
+  # lean:                      # Alternative object format (with toolchain pinning)
+  #   toolchain: "leanprover/lean4:v4.29.1"
 # env:                          # RESERVED: workflow-level environment variables (not yet implemented)
 #   CUSTOM_VAR: "value"
 mcp-servers:
@@ -460,6 +464,38 @@ When enabled, the compiler:
 - Auto-infers org from the git remote URL at compile time (overridable via `org:` field)
 - Fails compilation if org cannot be determined (no explicit override and no ADO git remote)
 
+### Runtimes Configuration
+
+The `runtimes` field configures language environments that are installed before the agent runs. Unlike tools (which are agent capabilities like edit, bash, memory), runtimes are execution environments that the compiler auto-installs via pipeline steps.
+
+Aligned with [gh-aw's `runtimes:` front matter field](https://github.github.com/gh-aw/reference/frontmatter/#runtimes-runtimes).
+
+#### Lean 4 (`lean:`)
+
+Lean 4 theorem prover runtime. Auto-installs the Lean toolchain via elan, extends the bash command allow-list, adds Lean-specific domains to the network allowlist, and appends a prompt supplement informing the agent that Lean is available.
+
+```yaml
+# Simple enablement (installs latest stable toolchain)
+runtimes:
+  lean: true
+
+# With options (pin specific toolchain version)
+runtimes:
+  lean:
+    toolchain: "leanprover/lean4:v4.29.1"
+```
+
+When enabled, the compiler:
+- Injects an elan installation step into `{{ prepare_steps }}` (runs before AWF network isolation)
+- Defaults to the `stable` toolchain; if a `lean-toolchain` file exists in the repo, elan overrides to that version automatically
+- Auto-adds `lean`, `lake`, and `elan` to the bash command allow-list
+- Adds Lean-specific domains to the network allowlist: `elan.lean-lang.org`, `leanprover.github.io`, `lean-lang.org`
+- Symlinks lean tools into `/tmp/awf-tools/` for AWF chroot compatibility
+- Appends a prompt supplement informing the agent about Lean 4 availability and basic commands
+- Emits a compile-time warning if `tools.bash` is empty (Lean requires bash access)
+
+**Note:** In the 1ES target, the bash command allow-list is updated but elan installation must be done manually via `steps:` front matter. The 1ES target handles network isolation separately.
+
 ### Target Platforms
 
 The `target` field in the front matter determines the output format and execution environment for the compiled pipeline.
@@ -1412,6 +1448,7 @@ When extending the compiler:
 4. **New template markers**: Handle replacements in the target-specific compiler (e.g., `standalone.rs` or `onees.rs`)
 5. **New safe-output tools**: Add to `src/safeoutputs/` — implement `ToolResult`, `Executor`, register in `mod.rs`, `mcp.rs`, `execute.rs`
 6. **New first-class tools**: Add to `src/tools/` — extend `ToolsConfig` in `types.rs`, wire in compilers
+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
 
 ### Security Considerations

examples/lean-verifier.md

@@ -0,0 +1,39 @@
+---
+name: "Lean Formal Verifier"
+description: "Analyzes code and builds formal Lean 4 proofs of critical invariants"
+engine: claude-opus-4.5
+schedule: weekly on friday around 17:00
+tools:
+  cache-memory: true
+runtimes:
+  lean: true
+safe-outputs:
+  create-pull-request:
+    target-branch: main
+  create-work-item:
+    work-item-type: Task
+    tags:
+      - formal-verification
+      - lean4
+permissions:
+  write: my-write-arm-connection
+---
+
+## Formal Verification Agent
+
+You are a formal verification agent. Your job is to analyze the codebase, identify critical invariants and safety properties, and build Lean 4 proofs that verify them.
+
+### Workflow
+
+1. **Identify invariants**: Review the source code for critical logic — data validation, state transitions, arithmetic bounds, access control checks.
+2. **Model in Lean**: Create `.lean` files that formalize the identified properties as Lean 4 theorems.
+3. **Prove correctness**: Write proofs for each theorem. Use `lake build` to verify the proofs compile.
+4. **Iterate on failures**: If a proof fails, analyze the error output from `lean` to understand why. Either fix the proof or report the property as unverifiable (which may indicate a bug).
+5. **Submit results**: Create a PR with the `.lean` proof files, or create work items for properties that could not be verified.
+
+### Guidelines
+
+- Start with the simplest invariants first (null checks, bounds checks, type safety).
+- Use `lake init` to create a new Lake project if one doesn't exist.
+- Check your memory for findings from previous runs to avoid re-analyzing the same code.
+- If a property cannot be formalized or proved, use the `create-work-item` tool to flag it for human review.

src/allowed_hosts.rs

@@ -139,4 +139,12 @@ mod tests {
         let hosts = mcp_required_hosts("unknown-mcp");
         assert!(hosts.is_empty());
     }
+
+    #[test]
+    fn test_lean_hosts() {
+        use crate::runtimes::lean::LEAN_REQUIRED_HOSTS;
+        assert!(LEAN_REQUIRED_HOSTS.contains(&"elan.lean-lang.org"));
+        assert!(LEAN_REQUIRED_HOSTS.contains(&"leanprover.github.io"));
+        assert!(LEAN_REQUIRED_HOSTS.contains(&"lean-lang.org"));
+    }
 }

src/compile/common.rs

@@ -484,25 +484,62 @@ pub fn generate_copilot_params(front_matter: &FrontMatter) -> Result<String> {
     }
 
     // Bash tool: use configured list, or defaults if not specified
-    let bash_commands: Vec<&str> = match front_matter.tools.as_ref().and_then(|t| t.bash.as_ref()) {
-        Some(cmds) if cmds.len() == 1 && cmds[0] == ":*" => {
-            // Unrestricted: single wildcard entry
-            allowed_tools.push("shell(:*)".to_string());
-            vec![]
-        }
-        Some(cmds) if cmds.is_empty() => {
-            // Explicitly disabled: no bash commands
-            vec![]
-        }
-        Some(cmds) => {
-            // Explicit list of commands
-            cmds.iter().map(|s| s.as_str()).collect()
-        }
-        None => {
-            // Default safe commands
-            DEFAULT_BASH_COMMANDS.to_vec()
+    let mut bash_commands: Vec<&str> =
+        match front_matter.tools.as_ref().and_then(|t| t.bash.as_ref()) {
+            Some(cmds) if cmds.len() == 1 && cmds[0] == ":*" => {
+                // Unrestricted: single wildcard entry
+                allowed_tools.push("shell(:*)".to_string());
+                vec![]
+            }
+            Some(cmds) if cmds.is_empty() => {
+                // Explicitly disabled: no bash commands
+                vec![]
+            }
+            Some(cmds) => {
+                // Explicit list of commands
+                cmds.iter().map(|s| s.as_str()).collect()
+            }
+            None => {
+                // Default safe commands
+                DEFAULT_BASH_COMMANDS.to_vec()
+            }
+        };
+
+    // Auto-add lean/lake/elan when runtimes.lean is enabled
+    let has_lean = front_matter
+        .runtimes
+        .as_ref()
+        .and_then(|r| r.lean.as_ref())
+        .is_some_and(|l| l.is_enabled());
+
+    let is_unrestricted_bash = front_matter
+        .tools
+        .as_ref()
+        .and_then(|t| t.bash.as_ref())
+        .is_some_and(|cmds| cmds.len() == 1 && cmds[0] == ":*");
+
+    if has_lean && !is_unrestricted_bash {
+        let bash_disabled = front_matter
+            .tools
+            .as_ref()
+            .and_then(|t| t.bash.as_ref())
+            .is_some_and(|cmds| cmds.is_empty());
+
+        if bash_disabled {
+            eprintln!(
+                "Warning: Agent '{}' has runtimes.lean enabled but tools.bash is empty. \
+                Lean requires bash access (lean, lake, elan commands).",
+                front_matter.name
+            );
+        } else {
+            for cmd in crate::runtimes::lean::LEAN_BASH_COMMANDS {
+                if !bash_commands.contains(cmd) {
+                    bash_commands.push(cmd);
+                }
+            }
         }
-    };
+    }
+
     for cmd in bash_commands {
         // Reject single quotes in bash commands — copilot_params are embedded inside
         // a single-quoted bash string in the AWF command.
@@ -1316,6 +1353,38 @@ mod tests {
         assert!(!params.contains("shell("));
     }
 
+    #[test]
+    fn test_copilot_params_lean_adds_bash_commands() {
+        let mut fm = minimal_front_matter();
+        fm.runtimes = Some(crate::compile::types::RuntimesConfig {
+            lean: Some(crate::runtimes::lean::LeanRuntimeConfig::Enabled(true)),
+        });
+        let params = generate_copilot_params(&fm).unwrap();
+        assert!(params.contains("shell(lean)"), "lean command should be allowed");
+        assert!(params.contains("shell(lake)"), "lake command should be allowed");
+        assert!(params.contains("shell(elan)"), "elan command should be allowed");
+        // Default bash commands should still be present
+        assert!(params.contains("shell(cat)"), "default commands should remain");
+    }
+
+    #[test]
+    fn test_copilot_params_lean_with_unrestricted_bash() {
+        let mut fm = minimal_front_matter();
+        fm.tools = Some(crate::compile::types::ToolsConfig {
+            bash: Some(vec![":*".to_string()]),
+            edit: None,
+            cache_memory: None,
+            azure_devops: None,
+        });
+        fm.runtimes = Some(crate::compile::types::RuntimesConfig {
+            lean: Some(crate::runtimes::lean::LeanRuntimeConfig::Enabled(true)),
+        });
+        let params = generate_copilot_params(&fm).unwrap();
+        assert!(params.contains("shell(:*)"), "unrestricted should be preserved");
+        // Should NOT add individual lean commands when unrestricted
+        assert!(!params.contains("shell(lean)"), "lean not needed with :*");
+    }
+
     #[test]
     fn test_copilot_params_custom_mcp_no_mcp_flag() {
         let mut fm = minimal_front_matter();