Uploading case study of using the bootstrap workflow

[Alan-Jowett]

This pull request adds a comprehensive case study documenting the process and results of extracting formal specifications for the ebpf_epoch module in the eBPF for Windows project. The document details each phase of the workflow, the parallel agent approach, audit findings, and lessons learned, providing a reproducible blueprint for future spec extraction efforts on complex systems code.

Key additions and themes:

Case study documentation:

• Adds a new case study markdown file, docs/case-studies/ebpf_epoch.md, describing the end-to-end process of extracting requirements, design, and validation specifications from the ebpf_epoch kernel module codebase.

Spec extraction workflow:

• Outlines a six-phase workflow including repository scan, parallel draft extraction by agents, human clarification, adversarial audit, human approval, and deliverable creation.
• Details the use of parallel agents to accelerate draft generation and describes the anti-hallucination guardrails and audit mechanisms for ensuring traceability and accuracy.

Results and findings:

• Summarizes quantitative outputs (e.g., number of requirements, test cases, audit findings) and presents a breakdown of what worked well and what could be improved in the process.
• Documents actionable lessons learned and provides guidance for reproducing the workflow on other modules. (F4bf52b7R

[Copilot]

Pull request overview

Adds a new documentation case study to PromptKit describing an end-to-end “spec extraction” workflow applied to the external ebpf_epoch module from the eBPF for Windows project, including phases, audit findings, and reproducibility guidance.

Changes:

• Add a detailed case study document covering a six-phase spec extraction workflow and outcomes.
• Document use of parallel background agents, traceability auditing, and lessons learned.
• Provide a reproduction section intended to guide readers applying the workflow elsewhere.

[Copilot]

The tables in this document use an extra leading | (e.g., || File | Lines | Role |), which renders as an empty first column in GitHub-flavored Markdown. Update these tables to standard Markdown table syntax (single leading/trailing pipe, no empty column) and apply consistently throughout the file (Input Files / Phase 2 / Findings / Deliverables / Quantitative Summary tables).

[Copilot]

This references a spec-extraction-workflow.md and a workflows/ directory, but this repository doesn’t appear to contain that file or directory. Please update the reproduction instructions to point to the actual PromptKit entrypoint/template(s) that readers should run (or link to the external project’s workflow if it lives outside this repo).

Suggested change

	To reproduce this extraction on another module:
	```
	Read and execute the spec-extraction-workflow in the workflows directory.
	```
	Then specify:
	- The source files to analyze
	- The output directory for specs
	- Any additional context files (design docs, related headers)
	The workflow is interactive and will pause at each phase gate for confirmation.
	To reproduce this extraction on another module using PromptKit:
	```bash
	# From the root of the PromptKit repository
	copilot -i "Read bootstrap.md and execute the prompt."

When the bootstrap prompt runs, indicate that you want to extract a specification
for a kernel module (for example, ebpf_epoch in the eBPF for Windows project),
and then specify:

• The source files to analyze
• The output directory for the generated specification documents
• Any additional context files (design docs, related headers)

The selected template will guide you through an interactive, gated workflow
similar to the one described in this case study, pausing at each phase gate for
confirmation.

[Copilot]

The objective section mentions the project’s spec-extraction-workflow.md, but there’s no such file in this repo. Consider either linking to the exact PromptKit template(s) used (e.g., the relevant templates/* entries) or explicitly stating that this workflow file lives in the target project repository (with a URL) to keep the case study reproducible.

Suggested change

	following the project's `spec-extraction-workflow.md`.
	following the project-specific spec extraction workflow defined in the
	[eBPF for Windows repository](https://github.com/microsoft/ebpf-for-windows).

[Copilot]

The “Deliverables” section lists paths like specs/epoch/requirements.md without clarifying whether these files exist in this PromptKit repo or were produced in the external eBPF for Windows repo. Please add a short note (and ideally links) indicating where these artifacts live so readers don’t expect them to be present here.

Suggested change

	These paths refer to files created in the external
	[eBPF for Windows](https://github.com/microsoft/ebpf-for-windows) repository
	as part of the draft PR #5150; they are not present in this PromptKit repository.