Install Lean Squad GitHub Agentic Workflow

[Copilot]

Summary

This PR installs Lean Squad on the JMC repository — a GitHub Agentic Workflow that progressively applies Lean 4 formal verification to the codebase, one target at a time.

Files Added

• .github/workflows/lean-squad.lock.yml — the compiled GitHub Actions workflow (generated by gh-aw v0.71.0, sourced from dsyme/raft-lean-squad as reference, pointing to githubnext/agentics/workflows/lean-squad.md@3de4e604)
• .github/workflows/lean-squad.md — the workflow prompt/description file (from githubnext/agentics), referenced at runtime by the workflow

Required Manual Steps After Merging

1. Set the COPILOT_GITHUB_TOKEN secret (required)

Go to Settings → Secrets and variables → Actions → New repository secret and add:

Secret name	Value
COPILOT_GITHUB_TOKEN	A GitHub personal access token (classic or fine-grained) that has GitHub Copilot access on your account. This is the token used to call GitHub Copilot's Claude Sonnet 4.6 model.

Note: Your Anthropic/Claude Code subscription provides access to Claude models via GitHub Copilot. The workflow uses GitHub Copilot's API (not the Anthropic API directly). The COPILOT_GITHUB_TOKEN must be a GitHub token for an account with a GitHub Copilot subscription that includes Claude model access.

Optional additional secrets (fall back to GITHUB_TOKEN if not set):

• GH_AW_GITHUB_TOKEN — a GitHub token with write access (for creating PRs/issues with more flexibility)
• GH_AW_GITHUB_MCP_SERVER_TOKEN — token for the GitHub MCP server
• GH_AW_CI_TRIGGER_TOKEN — token for triggering CI on created PRs

2. Create required labels (required)

Create the following labels in Issues → Labels → New label:

Label	Color	Description
automation	#0075ca	Automated changes
lean-squad	#7057ff	Lean Squad formal verification workflow
aeneas-bug	#d73a4a	Bug found by Aeneas/formal verification

Or via GitHub CLI:

gh label create automation --color 0075ca --description "Automated changes"
gh label create lean-squad --color 7057ff --description "Lean Squad formal verification workflow"
gh label create aeneas-bug --color d73a4a --description "Bug found by Aeneas/formal verification"

3. Enable workflow permissions (recommended)

In Settings → Actions → General → Workflow permissions, ensure:

• "Read and write permissions" is selected (allows the workflow to create PRs and issues)
• "Allow GitHub Actions to create and approve pull requests" is checked

How It Works

Once the secret is set, Lean Squad will:

• Run automatically every 8 hours on a schedule
• Be triggerable on-demand via /lean-squad <instructions> in any issue or PR comment
• Progressively work through 11 tasks: research → informal specs → Lean 4 specs → proofs → CI → reports
• Create PRs with formal verification artifacts in formal-verification/
• Maintain a rolling status issue [Lean Squad] Formal Verification Status
• Use memory/lean-squad branch for persistent memory across runs

Note on Engine

This workflow uses GitHub Copilot CLI with model claude-sonnet-4.6 (not the Anthropic API directly). Your Claude Code/Anthropic subscription provides access to Claude models through GitHub Copilot.

[joulook]

@copilot Please review this PR to make sure that it does not cause any security or any vulnerability issues or any other risks that can affect the main branch of JMC repository.

[Copilot]

Pull request overview

Installs the Lean Squad GitHub Agentic Workflow into the repository, including the human-readable workflow prompt and the compiled/pinned GitHub Actions workflow used to execute it.

Changes:

• Added the Lean Squad workflow prompt/config (lean-squad.md) used at runtime by gh-aw.
• Added the compiled/pinned gh-aw workflow (lean-squad.lock.yml) that runs on a schedule and on /lean-squad ... triggers.

Reviewed changes

Copilot reviewed 1 out of 2 changed files in this pull request and generated 3 comments.

File	Description
.github/workflows/lean-squad.md	Adds Lean Squad prompt/config, including safe-output limits and CI templates the agent will apply.
.github/workflows/lean-squad.lock.yml	Adds compiled GitHub Actions workflow generated by gh-aw that executes Lean Squad.

---

💡 Add Copilot custom instructions for smarter, more guided reviews. Learn how to get started.

[Copilot]

safe-outputs.max-patch-size is set to 10240 but the inline comment says “in kb, so 10MB”. In the same file, repo-memory.max-patch-size: 102400 is documented as 100KB, and the compiled workflow uses max_patch_size: 10240, which strongly suggests the unit is bytes (so this is a 10KB limit, not 10MB). This will likely prevent Lean Squad from creating PRs once changes exceed ~10KB. Please either correct the comment to match the actual unit/limit, or increase the value to the intended size (e.g., 10MB) and recompile the lock workflow.

Suggested change

	max-patch-size: 10240 # in kb, so 10MB
	max-patch-size: 10240 # 10KB max

[Copilot]

The compiled Safe Outputs config hard-caps create_pull_request.max_patch_size and push_to_pull_request_branch.max_patch_size to 10240 (10KB if this is bytes). This conflicts with the prompt’s “10MB” intent and is likely too small for most generated PRs, causing the workflow to fail when attempting to open/update PRs. If the intent is a larger cap, update safe-outputs.max-patch-size in lean-squad.md and re-run gh aw compile so this lock file reflects the correct limit.

Suggested change

{"add_comment":{"max":3,"target":"*"},"create_issue":{"labels":["automation","lean-squad","aeneas-bug"],"max":4,"title_prefix":"[Lean Squad] "},"create_pull_request":{"draft":false,"labels":["automation","lean-squad"],"max":2,"max_patch_size":10240,"protected_files":["package.json","bun.lockb","bunfig.toml","deno.json","deno.jsonc","deno.lock","global.json","NuGet.Config","Directory.Packages.props","mix.exs","mix.lock","go.mod","go.sum","stack.yaml","stack.yaml.lock","pom.xml","build.gradle","build.gradle.kts","settings.gradle","settings.gradle.kts","gradle.properties","package-lock.json","yarn.lock","pnpm-lock.yaml","npm-shrinkwrap.json","requirements.txt","Pipfile","Pipfile.lock","pyproject.toml","setup.py","setup.cfg","Gemfile","Gemfile.lock","uv.lock","CODEOWNERS","DESIGN.md","AGENTS.md","CLAUDE.md","GEMINI.md"],"protected_files_policy":"allowed","protected_path_prefixes":[".github/",".agents/",".githooks/",".husky/"],"title_prefix":"[Lean Squad] "},"create_report_incomplete_issue":{},"missing_data":{},"missing_tool":{},"noop":{"max":1,"report-as-issue":"true"},"push_repo_memory":{"memories":[{"dir":"/tmp/gh-aw/repo-memory/default","id":"default","max_file_count":100,"max_file_size":10240,"max_patch_size":102400}]},"push_to_pull_request_branch":{"if_no_changes":"warn","max":4,"max_patch_size":10240,"protected_files":["package.json","bun.lockb","bunfig.toml","deno.json","deno.jsonc","deno.lock","global.json","NuGet.Config","Directory.Packages.props","mix.exs","mix.lock","go.mod","go.sum","stack.yaml","stack.yaml.lock","pom.xml","build.gradle","build.gradle.kts","settings.gradle","settings.gradle.kts","gradle.properties","package-lock.json","yarn.lock","pnpm-lock.yaml","npm-shrinkwrap.json","requirements.txt","Pipfile","Pipfile.lock","pyproject.toml","setup.py","setup.cfg","Gemfile","Gemfile.lock","uv.lock","CODEOWNERS","DESIGN.md","AGENTS.md","CLAUDE.md","GEMINI.md"],"protected_files_policy":"allowed","protected_path_prefixes":[".github/",".agents/",".githooks/",".husky/"],"target":"*","title_prefix":"[Lean Squad] "},"report_incomplete":{},"update_issue":{"allow_body":true,"max":1,"target":"*","title_prefix":"[Lean Squad] "}}

{"add_comment":{"max":3,"target":"*"},"create_issue":{"labels":["automation","lean-squad","aeneas-bug"],"max":4,"title_prefix":"[Lean Squad] "},"create_pull_request":{"draft":false,"labels":["automation","lean-squad"],"max":2,"max_patch_size":10485760,"protected_files":["package.json","bun.lockb","bunfig.toml","deno.json","deno.jsonc","deno.lock","global.json","NuGet.Config","Directory.Packages.props","mix.exs","mix.lock","go.mod","go.sum","stack.yaml","stack.yaml.lock","pom.xml","build.gradle","build.gradle.kts","settings.gradle","settings.gradle.kts","gradle.properties","package-lock.json","yarn.lock","pnpm-lock.yaml","npm-shrinkwrap.json","requirements.txt","Pipfile","Pipfile.lock","pyproject.toml","setup.py","setup.cfg","Gemfile","Gemfile.lock","uv.lock","CODEOWNERS","DESIGN.md","AGENTS.md","CLAUDE.md","GEMINI.md"],"protected_files_policy":"allowed","protected_path_prefixes":[".github/",".agents/",".githooks/",".husky/"],"title_prefix":"[Lean Squad] "},"create_report_incomplete_issue":{},"missing_data":{},"missing_tool":{},"noop":{"max":1,"report-as-issue":"true"},"push_repo_memory":{"memories":[{"dir":"/tmp/gh-aw/repo-memory/default","id":"default","max_file_count":100,"max_file_size":10240,"max_patch_size":102400}]},"push_to_pull_request_branch":{"if_no_changes":"warn","max":4,"max_patch_size":10485760,"protected_files":["package.json","bun.lockb","bunfig.toml","deno.json","deno.jsonc","deno.lock","global.json","NuGet.Config","Directory.Packages.props","mix.exs","mix.lock","go.mod","go.sum","stack.yaml","stack.yaml.lock","pom.xml","build.gradle","build.gradle.kts","settings.gradle","settings.gradle.kts","gradle.properties","package-lock.json","yarn.lock","pnpm-lock.yaml","npm-shrinkwrap.json","requirements.txt","Pipfile","Pipfile.lock","pyproject.toml","setup.py","setup.cfg","Gemfile","Gemfile.lock","uv.lock","CODEOWNERS","DESIGN.md","AGENTS.md","CLAUDE.md","GEMINI.md"],"protected_files_policy":"allowed","protected_path_prefixes":[".github/",".agents/",".githooks/",".husky/"],"target":"*","title_prefix":"[Lean Squad] "},"report_incomplete":{},"update_issue":{"allow_body":true,"max":1,"target":"*","title_prefix":"[Lean Squad] "}}

[Copilot]

The Lean CI template written in Task 9 restricts push.branches to main, but this repo’s existing CI workflow targets master (see .github/workflows/gradle.yml:11-14). If Lean Squad generates lean-ci.yml as-is, it likely won’t run on default-branch pushes. Consider removing the branch filter entirely (path filtering already limits scope) or setting it to master/the repository default branch when generating the workflow.

Suggested change

	branches:
	- main

[Copilot]

@copilot Please review this PR to make sure that it does not cause any security or any vulnerability issues or any other risks that can affect the main branch of JMC repository.

Here is a thorough security review of the two files added by this PR.

---

Security Review: lean-squad.lock.yml + lean-squad.md

✅ Protections in Place

1. All dependencies pinned by immutable hash
Every GitHub Action is pinned by commit SHA (not a mutable tag), and every Docker container image is pinned by digest SHA. This eliminates supply-chain risk from a dependency being silently changed after pinning.

# Actions: SHA-pinned
uses: actions/checkout@de0fac2e4500dabe0009e67214ff5f5447ce83dd # v6.0.2
uses: actions/github-script@3a2844b7e9c422d3c10d287c895573f7108da1b3 # v9
# Containers: digest-pinned
ghcr.io/github/gh-aw-firewall/agent:0.25.28@sha256:a8834e285807654bf680154faa710d43fe4365a0868142f5c20e48c85e137a7a

2. AI agent runs inside a network-firewalled Docker sandbox
The Copilot CLI agent runs inside the awf (Agentic Workflow Firewall) container. Outbound network access is restricted to an explicit allowlist (GitHub, Lean ecosystem, Rust crates, LaTeX CTAN, arxiv.org, etc.). Arbitrary internet access is blocked.

3. AI agent cannot directly call GitHub APIs
All write operations (creating PRs, issues, comments) go through a "Safe Outputs" gateway — a rate-limited JSONL mechanism processed by a separate trusted job. The agent cannot write more than: 2 PRs, 4 issues, 3 comments, and 4 branch pushes per run. The GitHub MCP Server available to the agent is configured with GITHUB_READ_ONLY: "1".

4. Sensitive tokens excluded from the agent sandbox
COPILOT_GITHUB_TOKEN, GITHUB_MCP_SERVER_TOKEN, and MCP_GATEWAY_API_KEY are explicitly excluded from the AWF container (--exclude-env). The agent's Copilot API key and the GitHub write token are not accessible inside the sandbox.

5. Slash-command access control
When triggered via /lean-squad in a comment, the pre_activation job checks that the actor has admin, maintainer, or write role on the repository. External contributors cannot trigger the workflow.

6. Prompt injection / XPIA protections
User-supplied content (issue body, PR body, comment body) is passed through compute_text.cjs (sanitization) before reaching the agent. The system prompt includes an XPIA (cross-prompt injection attack) guard loaded from ${RUNNER_TEMP}/gh-aw/prompts/xpia.md.

7. No direct push to default branch
The agent only creates PRs. All code changes require human review and merge. The workflow cannot push directly to main.

8. persist-credentials: false on all checkouts
Git credentials are not persisted in the workspace after checkout, reducing the attack surface.

9. Concurrency groups
Concurrent runs are prevented, so a rapid series of slash-commands cannot spawn multiple simultaneous agents consuming secrets or credits in parallel.

---

⚠️ Risks to Be Aware Of

1. Agent can write files to .github/workflows/ (by design)
The safe-outputs config uses "protected_files_policy": "allowed" for .github/ path prefix — this is intentional for Task 9 (CI Automation), which needs to create lean-ci.yml. Any [Lean Squad]-prefixed PRs touching .github/ should be reviewed carefully before merging.

2. Prompt injection via repository content
The agent reads files from your repository (code, docs, existing FV artifacts) to do its job. A carefully crafted string embedded in a source file could attempt to redirect the agent. This is partially mitigated by the XPIA guard, the safe-outputs rate limits, and the fact that all output goes through PR review. However it cannot be fully eliminated in any LLM-based agentic workflow.

3. Scheduled execution costs
The workflow runs every 8 hours (3×/day) automatically, consuming GitHub Actions minutes and Copilot API tokens. No adverse security risk, but worth noting for budget/billing.

4. poutine:ignore annotations
A few steps suppress Poutine supply-chain warnings (# poutine:ignore untrusted_checkout_exec). These are all executing scripts from ${RUNNER_TEMP}/gh-aw/actions/ — populated by the SHA-pinned github/gh-aw-actions/setup action — not from the repository checkout. The suppression is legitimate but the scripts themselves are third-party code running on your runner with full runner permissions before the agent sandbox starts.

---

Summary

This PR does not introduce risks to the main branch. All agent-produced changes require human-approved PRs. The gh-aw framework has purpose-built security controls (firewall, safe-outputs gateway, token exclusion, membership checks, SHA-pinned dependencies) that are significantly stronger than a typical hand-written automation workflow. The risks noted above are inherent to any LLM agentic system of this class.

Recommended precaution: enable branch protection rules on main requiring PR review approval, if not already configured — this ensures even a compromised agent cannot merge its own PRs.