docs: use-case reference -- catch, prove, fix, re-verify absence (+ GitHub Actions example) [skip ci]

The loop: catch a regression in the diff, prove it with a reproducible check,
the dev/agent fixes it (tool gives a repair direction + the failing proof, not an
auto-patch), then the same proof re-runs and no longer triggers = absence
demonstrated by execution; the proof becomes a committed regression test. Example
GitHub Actions workflow uses the real 'ousast pre-push . --base --head --deadline
--mode --artifact' entry; PR-comment formatter marked as a placeholder. Honest
status separates what exists (re-verify by construction, --base/--head) from
delivery work (PR formatter, auto-landing the regression test) and the open
large-repo latency.

Co-Authored-By: Claude Opus 4.8 <[email protected]>

docs/use-case-fix-and-reverify.md

@@ -0,0 +1,98 @@
+# Use case: catch, prove, fix, re-verify
+
+The tool closes the loop on a security regression. It finds the problem in your
+change, proves it with a reproducible check, and after the fix re-runs that same
+check to confirm the problem is gone. The proof becomes a regression test. It
+does not write the patch for you; it hands you a failing check and a repair
+direction, and your fix is confirmed when the check turns green.
+
+## The loop
+
+1. **Catch.** On the changed code, the static arm flags a likely regression with
+   a location and a repair direction.
+2. **Prove.** Where the app is runnable, the proof arm builds and runs it and
+   demonstrates the issue: a check that triggers the effect on the current code.
+3. **Fix.** You, or a coding agent, write the fix against the repair direction
+   and the failing check. The tool does not generate the patch.
+4. **Re-verify absence.** The same proof is re-run against the fixed code. It no
+   longer triggers. That is the bug's absence demonstrated by execution, not a
+   claim that it "looks fixed."
+5. **Keep it.** The proof is a regression test. Commit it and the fix stays fixed.
+
+## What "re-verify absence" means, precisely
+
+A demonstrated finding is a differential: the proof triggers the effect on the
+vulnerable code and does not on the fixed code. Re-verifying a fix is the same
+operation run against your new revision. No effect means the specific issue the
+proof captured is gone. It does not claim the code is secure in general; it
+confirms that this proven issue no longer reproduces. That scoping is the point:
+it is honest about exactly what it checked.
+
+## What it does and does not do
+
+- It produces a repair direction and a failing proof, not an auto-generated patch.
+- It re-verifies the fix by re-running the proof; the verifier already runs a
+  demo against a given revision, so this is the existing mechanism, not a new one.
+- Families without a runnable proof (for example access control or configuration)
+  get the catch and the repair direction but no execution proof, and are advisory
+  only.
+
+## In CI, with GitHub Actions
+
+`ousast pre-push . --base <rev> --head <rev> --deadline <seconds>` runs an
+explicit base-versus-head check, which is what an Action calls on a pull request.
+The example below is reference material, not an active workflow in this repo.
+
+```yaml
+# .github/workflows/pre-push-security.yml  (example; adapt and enable in your repo)
+name: pre-push security
+on:
+  pull_request:
+jobs:
+  check:
+    runs-on: ubuntu-latest
+    steps:
+      - uses: actions/checkout@v4
+        with:
+          fetch-depth: 0            # base and head must both be present
+      - name: Install OpenUltraSAST
+        run: pipx install openultrasast   # or your pinned distribution
+      - name: Check the diff
+        env:
+          # model keys and spend caps, if the proof arm is used, come from secrets
+          DEEPSEEK_API_KEY: ${{ secrets.DEEPSEEK_API_KEY }}
+        run: |
+          ousast pre-push . \
+            --base "origin/${{ github.base_ref }}" \
+            --head "${{ github.sha }}" \
+            --deadline 300 \
+            --mode advisory \
+            --artifact "$GITHUB_WORKSPACE/pre-push.json"
+      - name: Comment findings on the PR
+        if: always()
+        run: |
+          # Placeholder: read pre-push.json and post the finding, its proof and the
+          # repair direction as a PR comment. This formatter is not packaged yet
+          # (see Honest status); wire your own, e.g. with gh pr comment.
+          cat "$GITHUB_WORKSPACE/pre-push.json"
+```
+
+The intended flow on a repository:
+
+- A pull request scans base to head. A demonstrated finding is posted as a PR
+  comment with its proof and repair direction, the evidence a developer takes to
+  a product owner to win capacity.
+- The fix pull request re-runs the check. The proof flips from failing to
+  passing, which is the fix confirmed.
+- The proof is committed as a regression test so the issue cannot return
+  unnoticed.
+
+## Honest status
+
+Re-verify by execution and the `--base/--head` entry point exist today. The
+turnkey pieces around them are delivery work, not detection: the PR-comment
+formatter and the automatic landing of a proof as a committed regression test are
+not packaged yet, and the base-versus-head path inherits the open large-repo
+latency limit, so a long deadline or a cluster lane may be needed on big diffs.
+The full-repository CI scan (as opposed to a diff) is roadmap work
+(`plane-on-kubernetes`), not the pre-push diff path shown here.