marius/Open_Ultra_SAST
1
0
Fork 0
mirror of https://github.com/norandom/OpenUltraSAST.git synced 2026-10-16 03:49:26 +00:00
Code Issues Packages Projects Releases Wiki Activity

spec(proof-arm-opencode): OpenCode MCP is the endpoint for PoC AND fix [skip ci]

Browse Source 
Maintainer direction: the same agentic endpoint authors the PoC, writes a candidate
fix against the repair direction + failing PoC, and hands it to the differential
verifier, which re-runs the PoC and confirms absence. Closes the no-auto-patch gap:
the proof is the acceptance test for the fix (a wrong fix is caught), the fix stays a
developer-reviewed proposal, and the green proof is the objective signal. Specced
alongside proof authoring, after qualification.

Co-Authored-By: Claude Opus 4.8 <[email protected]>
This commit is contained in:
Marius Ciepluch
2026-10-07 17:34:52 +02:00
co-authored by Claude Opus 4.8
parent 7f8a492857
commit 56cde9f535
1 changed files with 18 additions and 1 deletions
Download Patch File Download Diff File Expand all files Collapse all files
.kiro/specs/proof-arm-opencode/brief.md
+18 -1
View File
@@ -81,7 +81,24 @@ in a **gVisor-isolated** corpus, to demonstrate a regression before push. Guardr
scratch/egress limits), or does it need a new task kind?
5. Cost envelope per proof vs the current DeepSeek authoring.
## OpenCode MCP as the endpoint for both PoC and fix
Maintainer note (2026-10-07): OpenCode MCP is a good server endpoint for the PoC **and** the fix,
not only proof authoring. The same agentic endpoint can:
1. Author the PoC (the demonstrated proof) for a caught finding.
2. Write a candidate fix against the finding's repair direction and the failing PoC.
3. Hand the fix back to the differential verifier, which re-runs the PoC and confirms absence
(the proof flips from failing to passing).
This turns the "no auto-patch" gap in `../../../docs/use-case-fix-and-reverify.md` into "the proof
endpoint also proposes the fix, and the fix is accepted only when the proof it generated goes green."
The PoC is the acceptance test for the fix, so a wrong fix is caught, not trusted. The fix stays a
proposal for the developer to review; the verifier's green proof is the objective signal, not the
model's say-so. This fix capability is specced alongside the proof authoring when this arm is built.
## Not in scope
Changing the search arm, the oracle differential, or the abstract-interpretation triage. This brief
is only about the **proof-authoring** driver and its learning loop.
is about the **proof-authoring and fix** driver and its learning loop, planned as a full spec after
the safety net is qualified.