[Pedro Henrique Penna (ppenna)]

Installation

Install NFV's prototype PR reviewer using gh-aw v0.88.7.

• Target/base: microsoft/nvx, dev.
• Both workflow package pins and NFV_RELEASE_SHA: 498aad98c39314a8c55c89dff42d771276b957d8.
• Approved NFV_MODEL: gpt-5.6-sol.
• Both workflow Markdown files, generated locks (including action records), and the package record are included. Existing .gitattributes already marks workflow locks as generated and is unchanged.
• Default budgets and unrelated CI are unchanged. One existing test changed (tests-modified); no test data or test wiring changed:
  • WorkflowTests.test_only_the_report_job_writes_and_only_issues in scripts/test_nightly_ci.py allowed only nightly-ci-report.yml:report to write issues, so this PR failed NVX CLI on Linux and Windows. gh-aw v0.88.7 compiles the reviewer's add-comment safe output and default failure reporting into safe_outputs and conclusion jobs with issues: write, which post its PR comment and report its failures, missing tools, and incomplete runs as issues. The test now also expects those two jobs of nfv-pr-review.lock.yml, and doc/ci.md names them as the only other jobs that can write issues; every other workflow and job still cannot.
• Both required secret names are present; token validity, permissions, organization approval, and model access remain unproven.

Both workflows compiled successfully; Markdown links and the staged diff checks passed.

Keep this PR draft until nfv-pr-review.lock.yml is confirmed disabled_manually. Keep the reviewer disabled while marking ready and merging; do not require an NFV check on this installation PR. Merge requires explicit approval. After merge, recheck actual dev package pins, variables, and secret names before enabling the reviewer. A separate meaningful implementation-change pilot and its billable audit require separate authorization.

Findings are conditional MODEL refutations, not confirmed source bugs; failure to refute is not evidence of source correctness. No audit has been started.

[Pedro Henrique Penna (ppenna)]

Installation verification at captured PR head 9b8c619022568ae90b33a13a9295a1a8708896f3:

Check	Observed value
Target/base	microsoft/nvx / dev; this PR is draft
NFV_RELEASE_SHA	498aad98c39314a8c55c89dff42d771276b957d8, read back exactly
NFV_MODEL	gpt-5.6-sol, read back exactly
Package pins	Both installed workflow source: pins match that release at the captured head
Required secrets	COPILOT_GITHUB_TOKEN and NFV_RELEASE_TOKEN names present; validity, permissions, organization approval, and model access remain unproven
Reviewer	Workflow ID 406277038, state disabled_manually, verified after disabling via its registered ID

The initial filename-based disable returned 404 before registration; subsequent discovery by ID and disabling succeeded. The user explicitly chose to leave this PR draft and not merge. No activation or audit was started. Keep the reviewer disabled until an approved merge and verification against the actual default branch. A separate meaningful pilot and billable audit require separate authorization.

[Copilot]

🟡 Changes recommended

Colliding artifact names prevent retention of both usage snapshots, while equal job and audit timeouts leave no margin to upload evidence after an interrupted audit.

2 open issues

• Job timeout can prevent interrupted-audit evidence upload · New
• Duplicate usage artifact names cause caller upload failure · New

What changed in this PR

Installs NFV’s prototype PR reviewer alongside NVX’s existing CI, using a pinned workflow package and gh-aw v0.88.7. Its reports describe conditional model refutations, not confirmed source bugs.

Changes:

• Adds a source-context workflow that collects immutable PR changes and validates dependency lookup hints.
• Adds sandboxed Dafny analysis, evidence retention, and PR-comment publication.
• Records package provenance and generated workflow configuration without changing existing tests or unrelated CI.

File	Description
.github/​workflows/​nfv-source-context.md	Defines context collection, validation, and artifact handoff.
.github/​workflows/​nfv-source-context.lock.yml	Provides generated execution, sandboxing, and handoff jobs.
.github/​workflows/​nfv-pr-review.md	Defines the audit workflow and report publication.
.github/​aw/​packages/​microsoft-neuro-formal-verification-workflow-f129a0ff0f1c.json	Records the pinned package revision and workflow hashes.

_{Review effort: Balanced}

[github-actions]

This pull request changes existing tests

It modifies or removes 1 existing test asset(s), listed below. Review each with care: a change to a test can hide a regression that the test caught. See doc/contribute.md#changes-to-existing-tests.

Test code

Change	What	Before	After
modified test	def WorkflowTests.test_only_the_report_job_writes_and_only_issues in scripts/test_nightly_ci.py	scripts/test_nightly_ci.py:2024	scripts/test_nightly_ci.py:2024

Relocated unchanged: 0; added: 0. Compared the merge base 014128cb8196 with be760f5f11ee.

[Copilot]

🔵 Needs a closer look

The caller and reusable workflow upload the same artifact name, causing a hidden upload failure that omits the main review’s usage records from the cache fallback.

2 open issues

• Duplicate usage artifact names cause caller upload failure
• Job timeout can prevent interrupted-audit evidence upload

_{Review effort: Balanced}