SentinelOps-CI · fraware · Jul 16, 2026 · Jul 16, 2026 · Jul 16, 2026 · Jul 16, 2026
diff --git a/.github/dependabot.yml b/.github/dependabot.yml
@@ -16,3 +16,9 @@ updates:
     schedule:
       interval: weekly
     open-pull-requests-limit: 5
+
+  - package-ecosystem: github-actions
+    directory: "/"
+    schedule:
+      interval: weekly
+    open-pull-requests-limit: 5
diff --git a/.github/workflows/codeql.yml b/.github/workflows/codeql.yml
@@ -0,0 +1,40 @@
+name: CodeQL
+
+on:
+  push:
+    branches: [main, master]
+  pull_request:
+  schedule:
+    # Weekly Sunday 06:00 UTC
+    - cron: "0 6 * * 0"
+
+jobs:
+  analyze:
+    name: Analyze JavaScript/TypeScript
+    runs-on: ubuntu-latest
+    permissions:
+      actions: read
+      contents: read
+      security-events: write
+
+    strategy:
+      fail-fast: false
+      matrix:
+        language: [javascript-typescript]
+
+    steps:
+      - name: Checkout
+        uses: actions/checkout@v4
+
+      - name: Initialize CodeQL
+        uses: github/codeql-action/init@v3
+        with:
+          languages: ${{ matrix.language }}
+
+      - name: Autobuild
+        uses: github/codeql-action/autobuild@v3
+
+      - name: Perform CodeQL Analysis
+        uses: github/codeql-action/analyze@v3
+        with:
+          category: "/language:${{ matrix.language }}"
diff --git a/.github/workflows/lean4-ci.yml b/.github/workflows/lean4-ci.yml
@@ -6,13 +6,15 @@ on:
       - "specs/**"
       - "lakefile.lean"
       - "lean-toolchain"
+      - "src/lean4-generator.ts"
       - ".github/workflows/lean4-ci.yml"
   push:
     branches: [main, master]
     paths:
       - "specs/**"
       - "lakefile.lean"
       - "lean-toolchain"
+      - "src/lean4-generator.ts"
 
 jobs:
   lean4-specs:
@@ -31,6 +33,44 @@ jobs:
           auto-config: "true"
           test: "false"
 
+      - name: Report sorry count
+        env:
+          # Fail the job only when SPECSYNC_PROOF_GATE=strict (repo variable or secret).
+          SPECSYNC_PROOF_GATE: ${{ vars.SPECSYNC_PROOF_GATE || 'soft' }}
+        run: |
+          set -euo pipefail
+          if [ ! -d specs ]; then
+            echo "No specs/ directory — nothing to report"
+            exit 0
+          fi
+          # Count sorry tokens outside comments (block /- -/ and line --).
+          # Note: avoid embedding nested /- -/ examples inside docs (breaks strip).
+          TOTAL=$(python3 - <<'PY'
+import re, pathlib
+text = ""
+for p in pathlib.Path("specs").rglob("*.lean"):
+    text += p.read_text(encoding="utf-8", errors="ignore") + "\n"
+# Remove block comments iteratively so nested markers in docs do not leak tokens.
+prev = None
+while prev != text:
+    prev = text
+    text = re.sub(r"/-.*?-/", " ", text, count=1, flags=re.S)
+stripped = re.sub(r"--[^\n]*", " ", text)
+print(len(re.findall(r"(?:^|[^A-Za-z0-9_])sorry(?=[^A-Za-z0-9_]|$)", stripped)))
+PY
+)
+          TOTAL=${TOTAL:-0}
+          echo "SpecSync Lean sorry count: ${TOTAL}"
+          echo "sorry_count=${TOTAL}" >> "$GITHUB_STEP_SUMMARY"
+          echo "### SpecSync Lean \`sorry\` report" >> "$GITHUB_STEP_SUMMARY"
+          echo "" >> "$GITHUB_STEP_SUMMARY"
+          echo "Found **${TOTAL}** \`sorry\` occurrence(s) under \`specs/\`." >> "$GITHUB_STEP_SUMMARY"
+          echo "Gate: \`SPECSYNC_PROOF_GATE=${SPECSYNC_PROOF_GATE}\` (fail only when \`strict\`)." >> "$GITHUB_STEP_SUMMARY"
+          if [ "$SPECSYNC_PROOF_GATE" = "strict" ] && [ "$TOTAL" -gt 0 ]; then
+            echo "SPECSYNC_PROOF_GATE=strict and sorry found — failing"
+            exit 1
+          fi
+
       - name: Comment on PR with build summary
         if: github.event_name == 'pull_request' && success()
         uses: actions/github-script@v7

diff --git a/.github/workflows/node-ci.yml b/.github/workflows/node-ci.yml
@@ -36,5 +36,54 @@ jobs:
       - name: Build
         run: npm run build
 
-      - name: Test
-        run: npm test
+      - name: Test with coverage gate
+        run: npm run test:coverage
+
+      - name: Production dependency audit
+        run: npm audit --omit=dev --audit-level=high
+
+  docker-smoke:
+    runs-on: ubuntu-latest
+    permissions:
+      contents: read
+
+    steps:
+      - name: Checkout
+        uses: actions/checkout@v4
+
+      - name: Build Docker image
+        run: docker build -t specsync:ci .
+
+      - name: Smoke — image has compiled entrypoint
+        run: |
+          docker run --rm --entrypoint node specsync:ci -e "require('fs').accessSync('dist/index.js')"
+
+  vscode-extension:
+    runs-on: ubuntu-latest
+    permissions:
+      contents: read
+    defaults:
+      run:
+        working-directory: vscode-extension
+
+    steps:
+      - name: Checkout
+        uses: actions/checkout@v4
+
+      - name: Setup Node.js
+        uses: actions/setup-node@v4
+        with:
+          node-version: "22"
+          cache: npm
+          cache-dependency-path: vscode-extension/package-lock.json
+
+      - name: Install extension deps
+        run: |
+          if [ -f package-lock.json ]; then
+            npm ci
+          else
+            npm install
+          fi
+
+      - name: Compile extension
+        run: npm run compile
diff --git a/README.md b/README.md
@@ -14,7 +14,7 @@
 
 **Formal specs, meet your pull requests.**
 
-A GitHub App that turns diffs into structured specification suggestions—powered by LLMs, grounded in AST analysis, and wired for Lean 4 when you want proofs to compile.
+A GitHub App that turns PR diffs into structured specification suggestions—powered by LLMs when configured, grounded in tree-sitter AST analysis, and able to write Lean 4 **spec-as-contract** modules under `.specsync/` (opaque stubs + closed proofs where possible; labeled unfinished goals otherwise — not claimed complete).
 
 [![License: MIT](https://img.shields.io/badge/License-MIT-blue.svg)](LICENSE)
 [![TypeScript](https://img.shields.io/badge/TypeScript-5.x-3178c6?logo=typescript&logoColor=white)](https://www.typescriptlang.org/)
@@ -29,60 +29,65 @@ A GitHub App that turns diffs into structured specification suggestions—powere
 
 ## What it does
 
-| Capability               | Description                                                                                      |
-| ------------------------ | ------------------------------------------------------------------------------------------------ |
-| **Event-driven**         | Listens on GitHub for pull requests, pushes, and comments—then runs the analysis pipeline.       |
-| **Multi-language diffs** | Parses changes across common languages using Tree-sitter–backed extraction.                      |
-| **LLM-assisted specs**   | Proposes preconditions, postconditions, invariants, and rationale where API keys are configured. |
-| **Lean-ready output**    | Generated modules can target your Lake `specs/` tree so `lake build` stays honest.               |
-| **Operator-friendly**    | Health and readiness routes on the Probot router, Docker image, and CI for Node + Lean.          |
+| Capability | Description |
+| --- | --- |
+| **Async PR analysis** | Webhooks enqueue work on an in-process `AnalysisJobQueue` (idempotent per PR head SHA) so GitHub gets a fast ack. Optional `SPECSYNC_JOB_MARKERS_DIR` shares completion markers across instances on a volume (not committed to the target repo). |
+| **Multi-language diffs** | Tree-sitter AST for JavaScript, TypeScript, Python, Java, and Rust (no Go/C/C++ parsers). Review comments use `RIGHT` for adds/modifies and `LEFT` for pure deletions. |
+| **LLM-assisted specs** | Proposes preconditions, postconditions, invariants, and rationale when API keys are set. Production denies silent mock output unless `SPECSYNC_ALLOW_MOCK_LLM=true`. |
+| **`.specsync/` store** | `/specsync accept` commits JSON contracts (and Lean stubs) under `.specsync/` on the PR branch. Mutating commands require write AuthZ and are rate-limited per actor/PR. |
+| **Soft proof gate** | Default `SPECSYNC_PROOF_GATE=soft`: Lean CI **reports** `sorry` count (comments stripped). Set `strict` to **fail** on any remaining `sorry` in `specs/`. Closed fragments use real proofs (`trivial`, `Nat.zero_le`); unfinished LLM obligations stay labeled — this is not end-to-end formal verification. |
+| **Drift on push** | Compares changed functions against accepted `.specsync/` specs on main/master pushes. |
+| **Operator-friendly** | `GET /health`, `GET /ready` (includes job + metrics counters), optional secret-gated dashboard (loopback by default), Docker image, Node + Lean + CodeQL + VS Code extension CI. |
 
-The optional [VS Code extension](vscode-extension/) adds editor-side commands and local proof hooks; the server-side app lives in this repository’s `src/` tree.
+The optional [VS Code extension](vscode-extension/) reads the same `.specsync/` store; compile it with `npm run compile` in that folder.
 
 ---
 
 ## Architecture
 
-At a glance: GitHub sends webhooks to **Probot**; the app parses diffs, walks ASTs, asks the **spec analyzer** (and **LLM client** when configured), then posts back via the **GitHub UI** layer. Lean artifacts and CI are first-class paths, not an afterthought.
+GitHub webhooks hit **Probot**; handlers enqueue analysis, then the worker parses diffs, walks ASTs, calls the **spec analyzer** / **LLM client**, and posts review comments plus coverage checks. Accepted specs live under **`.specsync/`**; Lake-built Lean sources for this repo also live under [`specs/`](specs/).
 
 ```mermaid
 flowchart TB
   subgraph ingest [GitHub]
     E[Webhooks]
   end
   subgraph pipeline [Analysis]
+    Q[AnalysisJobQueue]
     D[Diff parser]
     T[AST extractor]
     N[Spec analyzer]
     L[LLM client]
   end
   subgraph surface [Surfaces]
     G[PR comments and checks]
-    K[Lean specs under specs/]
-    S[Slack and dashboards]
+    S[".specsync/ store"]
+    K[Lean stubs / Lake specs]
   end
-  E --> D --> T --> N
+  E --> Q --> D --> T --> N
   N --> L
   N --> G
-  N --> K
-  N --> S
+  G --> S
+  S --> K
 ```
 
-Formal modules consumed by Lake live under [`specs/`](specs/), with [`lakefile.lean`](lakefile.lean) and [`lean-toolchain`](lean-toolchain) pinning the toolchain.
+Formal modules consumed by Lake live under [`specs/`](specs/), with [`lakefile.lean`](lakefile.lean) and [`lean-toolchain`](lean-toolchain) pinning the toolchain. Generated accept-path Lean may also land under `.specsync/lean/` depending on configuration.
 
 ---
 
 ## Repository layout
 
-| Location                                   | Role                                                                             |
-| ------------------------------------------ | -------------------------------------------------------------------------------- |
-| [`src/index.ts`](src/index.ts)             | Probot entry: webhooks, `GET /health`, `GET /ready` when the router is available |
-| [`src/`](src/)                             | Application modules—parser, analyzer, GitHub UI, LLM client, generators          |
-| [`dist/`](dist/)                           | Build output from `npm run build` (generated, not committed)                     |
-| [`specs/`](specs/)                         | Lean 4 sources for `lake build`                                                  |
-| [`test/`](test/)                           | Jest tests (`*.test.ts`)                                                         |
-| [`vscode-extension/`](vscode-extension/)   | Editor extension (TypeScript → `out/`)                                           |
-| [`.github/workflows/`](.github/workflows/) | Continuous integration                                                           |
+| Location | Role |
+| --- | --- |
+| [`src/index.ts`](src/index.ts) | Probot entry: webhooks, queue, `GET /health`, `GET /ready` |
+| [`src/analysis-queue.ts`](src/analysis-queue.ts) | In-process async job runner with idempotency |
+| [`src/spec-store.ts`](src/spec-store.ts) | `.specsync/` read/write helpers |
+| [`src/`](src/) | Parser, analyzer, GitHub UI, LLM client, generators, metrics |
+| [`dist/`](dist/) | Build output from `npm run build` (generated, not committed) |
+| [`specs/`](specs/) | Lean 4 sources for `lake build` |
+| [`test/`](test/) | Jest tests (`*.test.ts`) |
+| [`vscode-extension/`](vscode-extension/) | Editor extension (`npm run compile`) |
+| [`.github/workflows/`](.github/workflows/) | Node CI, Lean CI, CodeQL |
 
 ---
 
@@ -126,35 +131,24 @@ Optional but common:
 ```env
 OPENAI_API_KEY=...
 ANTHROPIC_API_KEY=...
-GITHUB_TOKEN=...
+GITHUB_TOKEN=...          # CLI/demo only; PR path uses installation octokit
 SPECS_DIR=specs
 PORT=3000
+SPECSYNC_ALLOW_MOCK_LLM=false
+SPECSYNC_PROOF_GATE=soft
+SPECSYNC_MAX_SPECS_PER_PR=10
+SPECSYNC_JOB_MARKERS_DIR=       # optional shared FS for multi-instance job idempotency
+SPECSYNC_COMMAND_RATE_LIMIT=10
+SPECSYNC_COMMAND_RATE_WINDOW_MS=60000
+SPECSYNC_DASHBOARD=0
+SPECSYNC_DASHBOARD_SECRET=
 ```
 
+See [`env.example`](env.example) and [`app.yml`](app.yml) for the full App permission set (`checks: write`, `contents: write` for accept commits, etc.).
+
 ### GitHub App manifest (reference)
 
-Use this shape when registering the app; point the webhook URL at your deployed Probot instance.
-
-```yaml
-name: SpecSync
-description: GitHub-native specification assistant
-url: https://github.com/your-org/specsync
-hook_attributes:
-  url: https://your-domain.com/webhook
-  content_type: json
-default_permissions:
-  contents: read
-  pull_requests: write
-  issues: write
-  metadata: read
-default_events:
-  - pull_request
-  - push
-  - issues
-  - issue_comment
-  - pull_request_review
-  - pull_request_review_comment
-```
+Use [`app.yml`](app.yml) when registering the app; point the webhook URL at your deployed Probot instance. Replace org/domain placeholders with your deployment.
 
 ---
 
@@ -180,28 +174,35 @@ default_events:
 When the Probot server exposes a router, the app registers:
 
 - `GET /health` — liveness
-- `GET /ready` — readiness (extend when you add databases or queues)
+- `GET /ready` — readiness, including analysis-queue stats and in-process metrics counters
 
 The [`Dockerfile`](Dockerfile) healthcheck expects `GET /health` on the process port (default `3000`).
 
 ---
 
 ## Lean and Lake
 
-- **CI:** [`lean4-ci.yml`](.github/workflows/lean4-ci.yml) runs `lake build` via [lean-action](https://github.com/leanprover/lean-action) when Lean-related paths change.
-- **Local:** From the repo root, `lake build` after installing Elan/Lean.
-- **Generator contract:** Output from [`src/lean4-generator.ts`](src/lean4-generator.ts) should respect `SPECS_DIR` (default `specs`) so files sit in the same Lake library as [`lakefile.lean`](lakefile.lean).
+- **CI:** [`lean4-ci.yml`](.github/workflows/lean4-ci.yml) runs `lake build` via [lean-action](https://github.com/leanprover/lean-action) when Lean-related paths or `src/lean4-generator.ts` change.
+- **Local:** From the repo root, `lake build` after installing Elan/Lean (see `lean-toolchain`).
+- **Committed baseline:** [`specs/Specs.lean`](specs/Specs.lean) + [`specs/Specs/ClosedNatContract.lean`](specs/Specs/ClosedNatContract.lean) are Std-only and **contain zero `sorry`** (opaque + closed proofs).
+- **Generator contract:** [`src/lean4-generator.ts`](src/lean4-generator.ts) emits Std-only Lake modules:
+  - Function under contract → `opaque` (no unfinished proof for missing bodies)
+  - Smoke / Nat nonneg / other decidable fragments → real proofs (`trivial`, `Nat.zero_le`, …)
+  - Undecided LLM postconditions → `/- SpecSync: unproved: <reason> -/` + `sorry` only
+- **Proof gate:** `SPECSYNC_PROOF_GATE=soft` (default) reports counts; `strict` fails if any `sorry` remains. SpecSync does **not** claim completed formal verification while open obligations exist.
+- **Accept path:** Artifacts for target repos are stored under `.specsync/` (separate from this repo’s `specs/` library).
 
 ---
 
 ## Continuous integration
 
-| Workflow                                         | Purpose                                    |
-| ------------------------------------------------ | ------------------------------------------ |
-| [`node-ci.yml`](.github/workflows/node-ci.yml)   | Lint, format check, typecheck, build, test |
-| [`lean4-ci.yml`](.github/workflows/lean4-ci.yml) | `lake build` for Lean specs                |
+| Workflow | Purpose |
+| --- | --- |
+| [`node-ci.yml`](.github/workflows/node-ci.yml) | Lint, format, typecheck, build, coverage tests, `npm audit --production`, Docker smoke, vscode-extension `compile` |
+| [`lean4-ci.yml`](.github/workflows/lean4-ci.yml) | `lake build` for Lean specs |
+| [`codeql.yml`](.github/workflows/codeql.yml) | CodeQL analysis for JavaScript/TypeScript |
 
-[`dependabot.yml`](.github/dependabot.yml) schedules weekly npm updates for the root package and [`vscode-extension/`](vscode-extension/).
+[`dependabot.yml`](.github/dependabot.yml) schedules weekly npm and GitHub Actions updates.
 
 ---
 
@@ -217,10 +218,12 @@ docker run -p 3000:3000 \
   -e APP_ID=<id> \
   -e PRIVATE_KEY=<pem-or-base64> \
   -e WEBHOOK_SECRET=<secret> \
+  -e NODE_ENV=production \
+  -e SPECSYNC_ALLOW_MOCK_LLM=false \
   specsync
 ```
 
-Add LLM keys the same way if you use live models in production.
+Add LLM keys the same way if you use live models in production. Without keys (and without `SPECSYNC_ALLOW_MOCK_LLM=true`), the app posts an LLM-unavailable notice instead of fake specs.
 
 ### Other platforms
 
@@ -230,17 +233,18 @@ Any environment that provides Node, `PORT`, Probot env vars, and a **public HTTP
 
 ## Usage notes
 
+- **Accept / ignore / edit:** Comment `/specsync accept` (or ignore/edit) on a suggestion; AuthZ requires a collaborator (or stronger) or PR committer. Accept writes `.specsync/specs/` + Lean stubs on the PR branch.
 - **Demos:** After `npm run build`, run `npm run demo` or `npm run ui-demo`.
-- **VS Code:** See [`vscode-extension/README.md`](vscode-extension/README.md) for building the extension (`npx tsc -p .` inside that folder).
-- **Lean:** Modules under `specs/` should pass `lake build`; proof sketches may use `sorry` until completed.
+- **VS Code:** See [`vscode-extension/README.md`](vscode-extension/README.md); CI runs `npm run compile` in that package.
+- **Lean:** Committed modules under `specs/` pass `lake build` with zero `sorry`. Accept-path sketches may still use labeled unfinished proofs until a human (or stronger autoformalization) closes them.
 
 ---
 
 ## Quality and security
 
-- Pull requests run lint, format, typecheck, build, and tests; Lean CI validates the Lake project.
-- Prefer Dependabot PRs and periodic `npm audit` before releases.
-- Probot uses structured logging; see [`src/health.ts`](src/health.ts) for optional standalone health HTTP.
+- PRs run lint, format, typecheck, build, coverage-gated tests, production `npm audit`, Docker image smoke, and extension compile; CodeQL runs on push/PR/schedule.
+- Structured logs (Probot `context.log` / shared pino) include job id, PR, latency, and LLM mock|live soft-cost fields where available.
+- Prefer Dependabot PRs; treat audit failures as blocking unless an exception is documented in the workflow.
 
 ---