mirror of
https://github.com/norandom/OpenUltraSAST.git
synced 2026-10-18 20:49:28 +00:00
35f942f4c8b7477b72af6d9639c2b60fd5b2cff5
16
Commits
| Author | SHA1 | Message | Date | |
|---|---|---|---|---|
|
|
c8d2fefbb8 |
docs(kiro): archive the superseded roadmap; status notes on specs
A4: roadmap-2026-09-04.md moves to .kiro/archive/steering/ so it no longer loads as steering (roadmap.md and safety-net.md replaced it); roadmap.md's pointer follows it. overview.md's spec table is recounted from tasks.md and spec.json (adds ai-service-plane, harnessx-removal, learned-decision-engine, pre-push-safety-net; drops the stale "active one"), and the module line now cites the regenerated audit: 150 modules, 145 load-bearing, 5 standalone, 0 orphaned; 1,964 tests collected. A5: a dated status note at the top of the requirements (or brief) of 16 specs: retired, superseded, dormant or complete, and for model-grounded-detection the removal of judge/calibrate/execution (closing the Req 10 execution-tier option). spec.json phase corrected to implementation-complete where every task is checked (model-grounded- detection, propose-adjudicate-prove, tree-sitter-overlay-extra, corpus-seeded-mechanisms, pair-corpus-honesty); openrouter-sast-harness gets a spec.json with status retired. Nothing deleted, no spec moved. Co-Authored-By: Claude Opus 5.5 <[email protected]> Claude-Session: https://claude.ai/code/session_01EmM1j46qgKMh3zqD1QMwEo |
||
|
|
64a27c4e30 |
docs(model-grounded-detection): record what 16/16 does and does not mean
Asked whether the prior spec is finished. Audited rather than counted, and the answer is: all 16 tasks are complete as written, and not all requirements are satisfied in the product. Four are built but unreachable, so the requirement is not met where it matters: model/report.py implements the per-slice and overfitting-gap discipline (Req 11.1) and has no production caller; resolve_execution_backend returns NullExecutionBackend on BOTH branches so the execution_confirmed rung (Req 10.1) can never be reached; harvest_recipe (Req 9.4) is a seam with nothing plugged into it; and the pipeline that measures 90.0% pair-correct is called only by a measurement harness, never by ousast scan. That is a spec defect rather than an execution one. No task ever said "make this reachable", and Req 11.2 -- the gates stay byte-identical -- is satisfied PRECISELY BECAUSE nothing is wired. I read that as reassurance for a whole session when it was evidence. The spec is not reopened; it remains the complete record of building and measuring the arbiter. contributor-scan takes all four: its Req 1 closes 8.x and 11.1 in the product, Req 7.1 forces the memory decision 10.1 defers, and Req 9 covers the harvest 9.4 left as a seam. Co-Authored-By: Claude Opus 5 (1M context) <[email protected]> Claude-Session: https://claude.ai/code/session_01T7XD7x5KonMdmGRkp63EQG |
||
|
|
0c71c956fd |
feat(model-grounded-detection): group 6, the execution tier as a seam not a build
The rung this project deliberately does not build. Clearwing already runs sandbox lifecycles, container pools, sanitizer images, PoC replay and stability classification, and the corrective brief concluded -- from this project's own defect history -- that reimplementing that machinery is where we go wrong. So model/execution.py decides eligibility, calls an adopted tool, and records what happened. A test asserts structurally that it imports no container or subprocess machinery and defines no build/run/compile/patch function, because the failure mode to prevent is this file quietly growing a sandbox. Eligibility is narrow in both directions: only a family a static model cannot arbitrate (memory safety in C, where the bug turns on runtime layout -- Req 10.3 forbids any web/logic family depending on this tier, and each now has taint, dominance or constant abstraction instead), and only a finding the model left undecided. The tier escalates uncertainty; it never re-checks a verdict. One deliberate asymmetry: a failure to reproduce is NOT a refutation. A sandbox that does not trigger a bug has not shown the bug is absent, only that this attempt did not trigger it, so the candidate stays where the model left it. Reading a failed reproduction as a clean bill of health is the same error class as reading an absent engine as "no vulnerability". With no adopted tool present -- the normal case -- the rung is never reached and clearwing_unavailable is recorded. All 16 tasks of model-grounded-detection are now done. 720 passing, mypy/ruff clean, gates byte-identical, zero orphaned modules. Co-Authored-By: Claude Opus 5 (1M context) <[email protected]> Claude-Session: https://claude.ai/code/session_01T7XD7x5KonMdmGRkp63EQG |
||
|
|
86f434ab89 |
docs(model-grounded-detection): tick 5.1/5.2 and record the closure-scoping fix
The boxes were left unticked and the notes unwritten when group 5 was committed. Records the closure fix and the three bugs it uncovered, each of which would have raised the number while making the answer untrue, and the correction that req.url was not a wrong diagnosis but an untestable one -- the scoping bug blocked everything downstream of it. Co-Authored-By: Claude Opus 5 (1M context) <[email protected]> Claude-Session: https://claude.ai/code/session_01T7XD7x5KonMdmGRkp63EQG |
||
|
|
91c0931a05 |
measure(model-grounded-detection): group 4 ceiling, 39.1% entailed against the flat IR's 2.2%
Full model layer over 92 pairs: 39.1% model_entailed (36/92), 45.6% reaching any verdict, 23.9% distinguished -- an 18x lift in entailment from an arbiter that makes no model calls at all. Per family: untrusted_destination 0.80 entailed, injection 0.58 (0.36 distinguished), deserialization 0.33, prototype 0.14, config_secrets 0.10, path 0.00. access_control reaches 6 of 8 pairs at 0.38 distinguished -- the class no crash oracle can reach, arbitrated deterministically. A hypothesis tested and discarded. From the group-2 misses I diagnosed path's 0/8 as a missing req.url source token and said so. The probe -- the same 8 pairs with and without the token -- returned 0/8 -> 0/8. Falsified. The real cause is that the sink sits lexically inside an anonymous callback, so its enclosing method is the closure (<lambda>0) and the sinkMethod == function filter drops it; verdict(function="") on the same CPG returns model_entailed. And the obvious fix for that is wrong. Relaxing the filter raises the number with a FALSE witness: the flows found in the closure are `res -> readFileSync` and `this -> ...`, neither of which is the vulnerability, whose real path crosses a helper (req.url -> url -> resolveUrl -> possibleFilename). Turning a miss into a wrong entailment is worse than the miss -- it is the arbiter asserting something untrue, the one failure mode this architecture exists to prevent. The correct fix is two-part and recorded: scope a sink to any method lexically nested in the labeled function, and scope parameter sources to that function's own parameters, then re-measure counting only real witnesses. Every miss is classified and none is architectural: 23 sink absent from the excerpt or unmodelled, 13 no recognisable source in the excerpt, 3 source unmodelled with the idiom named. Two honesty items in the artifact. 16 of 92 pairs carry no function label and are arbitrated over the whole file, so a verdict can credit a different finding than the labeled one -- owasp-python-hash (CWE-327) is credited for a permissive set_cookie elsewhere in its file, on both sides. And config_secrets conflates three abstractions: permissive setting values (implemented), weak algorithm choice (facts already carry weak_literals, unwired) and hardcoded secrets (needs a credential-literal check). 694 passing, mypy/ruff clean, gates byte-identical, zero orphaned modules. Co-Authored-By: Claude Opus 5 (1M context) <[email protected]> Claude-Session: https://claude.ai/code/session_01T7XD7x5KonMdmGRkp63EQG |
||
|
|
b8f8f727c6 |
feat(model-grounded-detection): group 3, the evidence ladder and the judge
3.1 adds StaticFinding.rung beside evidence_level rather than renaming it. The existing evidence_level carries `static_corroboration`, emitted by the flat IR overlay -- a path Req 4.4 demotes to the suspicion band. Restating that as model_corroborated would claim a CPG arbitrated something it never saw, and rewriting every legacy finding to suspicion would be a product-visible regression nobody asked for. So `rung` defaults to suspicion and is raised only by ladder.at_rung(finding, verdict), which is the structural form of Req 5.4: nothing rises above suspicion without a Verdict behind it. The witness travels with the rung, because a rung without its evidence is just a louder assertion. It reaches markdown, JSON and SARIF. 3.2 is the judge, and it is defined as much by what it lacks. Three exhaustive outcomes: the model entails (report it, never call the model), the model contradicts (drop the claim, record why), the model cannot decide (report suspicion). The LLM gets one bounded typed question with tools=[] so it cannot search for the site, asked only about the residual the graph cannot settle -- whether a sanitizer on a REAL flow suffices. Its answer can only confirm a flow the CPG already found; it can never conjure one. Req 8.5 is asserted structurally: a test parses judge.py and fails on any AST name like k_runs/majority/vote/average/acceptance/floor/budget, any for/while loop, or an import from the deleted round machinery. That test first matched the word "votes" in the module's own docstring, which is why it now inspects code rather than text. Verified live against a real CPG, not only scripted rows: vuln rung=model_entailed request.args["name"] -> db.execute(...) fixed rung=suspicion no source reaches this sink model calls made: 0 Both sides arbitrated by the graph with the LLM never consulted -- the thing the prior architecture could not do at any price. 678 passing, mypy/ruff clean, gates byte-identical, zero orphaned modules. Co-Authored-By: Claude Opus 5 (1M context) <[email protected]> Claude-Session: https://claude.ai/code/session_01T7XD7x5KonMdmGRkp63EQG |
||
|
|
7387d2f190 |
measure(model-grounded-detection): task 2.3 reads GO on Joern
Injection slice, 50 pairs, ~30 minutes of real engine time.
model_entailed on the vulnerable side 54% (27/50) vs the flat IR's 2.2%
... on minimal-fix pairs only 61.5% (16/26)
pairs distinguished 32% overall, 38.5% on minimal-fix
determinism (Req 6.4) every verdict identical on re-run
cost median 32s/pair, max 58s
CPG build failures 1
The engine is not the constraint: all 23 misses trace to our own data model --
11 sinks absent from the fact tables (Django ORM objects.raw, self.query,
GraphQL resolvers), 11 where the sink is modelled but no source reaches it, and
one C translation unit that does not parse standalone, counted separately so it
can never read as "no vulnerability". That is exactly the result that justifies
adopting a CPG rather than building one.
The finding that changes the design: classifying what the 50 injection FIXES
actually do gives other_or_validation 37, bound_parameters 10, argv_list 2,
sanitizer_call 1. The dominant fix is a validation guard on the path, not a
sanitizer and not a sink shape -- and taint reachability can never separate
those pairs, because the flow still reaches the sink and what changed is that a
guard now dominates the path. The arbiter must be TAINT + DOMINANCE, which is
the same primitive task 4.1 builds for access_control, with the guard
vocabulary ported in task 1.1 as its lookup list. Two planned mechanisms
collapse into one, and 4.1 should now precede the remaining TaintSpecs.
Reported per stratum because only 26 of 50 pairs are genuine minimal-fix pairs:
12 are different programs (local-python-vulnerable is 7% similar with 83
changed lines) and 12 are large rewrites. A raw distinguished_rate would
measure corpus quality and report it as model quality.
Also corrected in the notes: the Flask-shaped source table is a real gap but a
minor lever -- adding Django patterns would gain a source for exactly one pair.
Co-Authored-By: Claude Opus 5 (1M context) <[email protected]>
Claude-Session: https://claude.ai/code/session_01T7XD7x5KonMdmGRkp63EQG
|
||
|
|
1765e51da1 |
feat(model-grounded-detection): the safe-shape test, without which the model arbitrates nothing
The first live run produced the finding that shapes this design: taint
reachability alone does not distinguish a fix from a bug. On the canonical SQL
pair the flow request.args["name"] -> name -> execute exists on BOTH sides --
vuln db.execute("select ... '" + name + "'") one argument, interpolated
fixed db.execute("select ... = %s", (name,)) two arguments, bound
-- so the model entailed the fixed twin exactly as readily as the vulnerable
one, and arbitrated nothing. What separates them is the SHAPE of the sink call,
which is precisely what safe_shape_sinks preserved from the earlier sanitizer
fix. The query now reports sinkArity and sinkArg0Literal, and a flow ending at
a sink written in its declared-safe form is not a vulnerability.
Two bugs in that shape test, both found only against the real engine:
Joern's `call.argument` includes the RECEIVER at argumentIndex 0, so `db` was
counted as an argument -- making a one-argument interpolated call look like a
two-argument bound one, the exact inversion of the test -- and the "first
argument" whose literalness decides a format-string sink was the receiver
rather than the format. Both fixed with argumentIndexGt(0).
The rule is narrow on purpose: only sinks named in safe_shape_sinks are subject
to it (os.system(x) is not safe merely because it takes one argument), and a
row carrying no shape fields is judged on the flow alone -- an unknown shape
must never be read as a safe one.
End to end on the pair, deterministic and with no model call:
vuln -> model_entailed request.args["name"] -> db.execute(...) (line 4)
fixed -> None
Co-Authored-By: Claude Opus 5 (1M context) <[email protected]>
Claude-Session: https://claude.ai/code/session_01T7XD7x5KonMdmGRkp63EQG
|
||
|
|
9ed0e45c5f |
feat(model-grounded-detection): group 1, subtract the noise architecture
99 source modules -> 81. 832 tests -> 646. The whole learning/ package (16 modules, ~4,100 lines) and six semantic/ modules removed, with the three gates byte-identical to 2026-09-06-gate-baseline.txt at every step. The sequence is what made it safe: vocabularies ported first (1.1), importers detached second (1.2-1.3), deletion third (1.4). Every import break during the deletion was therefore a detachment miss in the importer and was fixed there -- no module was restored to satisfy one. Both misses were the same shape and were fixed as a class: operations.py and shapes.py each imported trailing_name from the deleted variants.py, so it moved to semantic/ir.py, its natural home, and both importers changed in one edit. Ported before deleting: the closed guard vocabulary (verbatim, nothing else holds it) into model/specs.py, which derives TaintSpec and DominanceSpec from the retained ruleset facts rather than copying them. Re-homed: families -> model/taxonomy, candidates -> model/candidates, endpoint -> model/endpoint, plus Region, labeled_family and labeled_spans. labeled_family no longer falls back to the LLM classifier -- an unlabeled pair is honestly unknown. Four deviations, each recorded in the spec notes with its reason. improve/ evolve.py and validator.py were stripped, not deleted: each mixes the mechanism lever (gone) with the deterministic rule-status loop `ousast improve` still runs, which has no LLM in it; a test now asserts the lever's absence by symbol so it cannot creep back. The learning CLI group became `model candidates`, because deleting it outright would have orphaned the retained enumerator by removing its only entry point. thinking moved from [learning] to [models]. A gap named rather than papered over: no retained sink fact routes by CWE to path, output_encoding, untrusted_destination or prototype -- the same hole the entailment ceiling diagnosed. The test asserts the seeded set and the gap set exactly, so task 4.2 must update it when it authors those sinks. The audit found exactly one genuine orphan: vectorstore.py, a bakeoff harness with no production caller and no CLI, alive only through its own test. The five named subsystems each carry an explicit decision. Manifest committed, with a test asserting the tree still matches it. Group 2 (the Joern go/no-go) has not started. Co-Authored-By: Claude Opus 5 (1M context) <[email protected]> Claude-Session: https://claude.ai/code/session_01T7XD7x5KonMdmGRkp63EQG |
||
|
|
fc4dab97fb |
docs(model-grounded-detection): attach Req 7.4 (verifier boundary) to task 1.1
The prior commit's edit did not match and 7.4 was left unclaimed. model/specs.py is read-only data -- no LLM and no optimiser writes it -- and task 1.1 now carries that criterion with a test asserting the module exposes no writer. All 49 criteria trace to a task. Co-Authored-By: Claude Opus 4.8 <[email protected]> Claude-Session: https://claude.ai/code/session_01T7XD7x5KonMdmGRkp63EQG |
||
|
|
6fe8682993 |
docs(model-grounded-detection): 16 tasks in 6 groups, with a coupling map so Opus does not crash-discover
Design approved. All 49 criteria trace to a task. The tasks carry an agent-guidance preamble aimed squarely at the escalations this session hit: the eighteen-defect lesson (fix the class, not the instance), the gate-baseline as the safety net (the whole learning/ package is off the gate path, so its deletion cannot move a gate -- a moved gate means you touched a retained path), the zero-dep capability-detection pattern to copy verbatim, and -- most important for the subtraction -- a full coupling map naming every touchpoint of the removed code (cli, pairs hunter path, config, reports, semantic seed/loo, the mechanism loop across improve/ and semantic/). The subtraction is not discovery by import error. Group 1 is pure gate-protected subtraction, sequenced so vocabularies are ported (1.1) and importers detached (1.2-1.3) before anything is deleted (1.4), then tests reduced in the same spirit (1.5) and the tree audited for orphans (1.6). Group 2 is a Joern go/no-go: task 2.3 reads go or stop, and groups 3-6 do not begin until it is green -- building past a red 2.3 is the mistake the whole spec exists to prevent. Parallelism is deliberately absent; the subtraction is sequential and the spike gates the rest. Not approved for implementation. Co-Authored-By: Claude Opus 4.8 <[email protected]> Claude-Session: https://claude.ai/code/session_01T7XD7x5KonMdmGRkp63EQG |
||
|
|
0a8cc9b5a7 |
docs(model-grounded-detection): design, subtraction first and a Joern spike that can stop it
Requirements approved. All 49 criteria trace to a component. The shape: a Code Property Graph (Joern) is the arbiter; taint reachability and guard dominance produce evidence-ladder verdicts (suspicion / corroborated / entailed / execution_confirmed); the LLM answers one bounded question per candidate and its claim is checked against the CPG, never averaged. Two design disciplines carried from the requirements: Phase 1 is subtraction, and it removes ~5,000 lines before a line of Joern is written. The learning/ noise architecture is absent from the gate path, so rounds/acceptance/proposer/journal, the K-run/floor/sign-test in scoring, and the mechanism loop delete without moving a gate -- proven by the committed gate-baseline run before and after, and by an import-graph check that fails the build if a removed module is still imported. The guard and sink vocabularies are ported into model/specs.py *before* their modules are deleted. Tests are reduced in the same change, with a test->requirement map. A module-audit manifest classifies all 99 modules and names fusion/mcp/skills/harness_ext/ hunter_harness for an explicit keep-or-remove decision. Phase 2 is a Joern spike on the injection family alone -- the CpgBackend seam (subprocess to joern-parse + a CPGQL query emitting JSON, out of process, one isolated touch-point) and one TaintSpec, end to end, with a determinism test. It can end the design before the integration cost is paid, the same way the candidate ceiling could have in the prior spec. Joern is capability-detected on PATH like the semantic extra; without it every verdict degrades to suspicion and the core stays zero-dependency. What survives re-homes under model/: the taxonomy, the candidate enumerator (suspicion band), the endpoint client, and the obligation facts feeding the dominance queries. Not approved. Co-Authored-By: Claude Opus 4.8 <[email protected]> Claude-Session: https://claude.ai/code/session_01T7XD7x5KonMdmGRkp63EQG |
||
|
|
1ef578f793 |
docs(model-grounded-detection): requirements, subtraction first
11 requirements, 49 criteria. The outgrowth is addressed head-on and it leads,
because building on a superseded 99-module / 832-test surface is how this
session logged eighteen defects.
Req 1-3 are subtraction and come first:
1 remove the noise architecture by name -- rounds, acceptance, proposer,
journal, the K-run/floor/sign-test in scoring, the mechanism lever and
shape-search loop -- preserving the security *models* they carried. The
whole learning/ noise layer is absent from the gate path, so it deletes
without moving a gate.
2 reduce the 832 tests to what protects surviving behavior: a test that
pinned a deleted mechanism dies with it, every survivor maps to a
surviving requirement, and the "does nothing / greps --help / passes with
the capability absent" tests are removed outright.
3 audit all 99 modules -- load-bearing / standalone / orphaned -- and delete
the orphans, with fusion/mcp/skills/harness_ext/hunter_harness named for
an explicit keep-or-remove decision.
Req 4-8 adopt the CPG arbiter: Joern behind an optional extra (core stays
zero-dep, degrades to suspicion without it), the evidence ladder as the verdict
type, deterministic taint-reachability and guard-dominance verdicts, our
taxonomy and source/sink/sanitizer/guard models ported to CPG queries, and the
LLM reduced to a proposer whose claim the model checks -- no K-runs, no floor,
no acceptance rule, no evolve loop. Req 9 makes the corpus the model's
calibration set (a pair the model can't split is a named model gap). Req 10
keeps execution as a deferred, adopted-from-Clearwing tier for memory/C only.
Not approved.
Co-Authored-By: Claude Opus 4.8 <[email protected]>
Claude-Session: https://claude.ai/code/session_01T7XD7x5KonMdmGRkp63EQG
|
||
|
|
a3945427ab |
docs(model-grounded-detection): IL not AST, and adopt the CPG engine (Joern)
Two design questions answered by the entailment measurement. IL, not AST. Our semantic/ir.py is a lossy AST projection -- flat call/bind lists, no CFG, no PDG -- which is *why* entailment is 2.2%. Guard dominance is a dominator-tree question and path-sensitive taint needs branch structure; a flat bind list expresses neither. Real abstract interpretation is a fixpoint over a CFG, so the substrate is a Code Property Graph: AST + CFG + PDG + call graph in one queryable graph, taint as source->sink-minus-sanitizer reachability, absence as dominance. Adopt, not build. Building a multi-language CFG/PDG/taint engine on tree-sitter is reinventing CodeQL/Semgrep/Joern -- the maximal case of this session's failure mode. Joern is Apache-2.0, covers our exact corpus (C/C++/Java/JS/Python/Kotlin/binary), has a taint engine, is embeddable, and a CPG+LLM MCP bridge already exists. The 2.2% on our flat IR is the measured distance to a real CPG, and closing it by hand is reimplementing Joern. The flow: source -> Joern CPG -> taint + dominance -> deterministic entailed/corroborated verdict -> LLM judges the residual, checked against the CPG. What stays ours is the contribution: the taxonomy and the source/sink/sanitizer/guard models for the web/logic CWEs, ported to CPG queries, plus the LLM-checked-against-the-model orchestration. Joern is a workbench with no opinion on these classes; that opinion is our layer. Named cost: Joern is JVM/Scala, so server-mode or the MCP bridge, not in-process. Three-layer adoption now: Joern CPG for the web/logic arbiter, Clearwing for the memory/C execution tier, and our security modelling + LLM orchestration as the layer that binds them. Co-Authored-By: Claude Opus 4.8 <[email protected]> Claude-Session: https://claude.ai/code/session_01T7XD7x5KonMdmGRkp63EQG |
||
|
|
9e811c1baf |
measure(model-grounded-detection): the entailment ceiling is 2.2%, and it is depth not a wall
The analogue of the candidate ceiling, one rung up: not "can a site be enumerated" (96.6%) but "can a deterministic abstract-interpretation model DECIDE the vulnerability without trusting the LLM". Offline, no model calls. model_entailed today 2.2% (2/92 web/logic pairs) model_corroborated, one-hop taint 24% (22/92) taint reachable, multi-hop 35% (26/74 flow families) candidate site enumerable 96.6% (for comparison) The gap between 96.6% and 2.2% is the gap between enumerating and arbitrating, and it is the finding. The model cannot be a pure arbiter at v1. But the measurement diagnoses depth, not impossibility: one-hop source resolution (real taint sits 1-3 binds upstream: q = '...'+id; execute(q)), a closed literal sink table (misses project wrappers and path/xss/prototype sinks), and a function-naming gap that eats 20/50 injection pairs. Deepening the taint to the candidate enumerator's depth-4 chain already moved injection 24% -> 48%. So the course is a layered arbiter, not a pure one: report model_entailed where the model proves it (deterministic, no LLM); let the LLM judge but check its claim against the resolved taint on the ~35% corroboration band (noise removed there); honest suspicion for the rest, which is where the deferred execution/differential tier earns its place. Modeling confirmed as abstract interpretation; SMT reserved for the memory/C tier; concolic avoided. Co-Authored-By: Claude Opus 4.8 <[email protected]> Claude-Session: https://claude.ai/code/session_01T7XD7x5KonMdmGRkp63EQG |
||
|
|
091303c7c0 |
docs(model-grounded-detection): the arbiter is a program model, not a sandbox
Maintainer correction: execution isn't possible for all SAST targets, and the bugs this project owns -- IDOR, missing authz, injection -- don't crash anything. Execution is the easy arbiter only for memory-safety-in-C, which is not our world. What execution provided was an independent, deterministic arbiter of whether a claim is real -- not the same LLM that made it, not a noisy vote. That arbiter can be built statically, from the code, as a program model the claim is checked against. LLM proposes; the model disposes. Same architecture, same repair of the root cause, no runnable target required. The evidence ladder becomes static and deterministic: suspicion -> model_corroborated (claim consistent with resolved dataflow / a guard its siblings carry is absent) -> model_entailed (the model alone establishes it) -> execution_confirmed (deferred tier, C memory-safety only). model_corroborated and above are deterministic -- run the checker twice, same verdict -- which removes the run-to-run noise the same way a crash would, with no K-runs and no target to build. Our IR candidate enumerator (96.6% ceiling), binding chains and obligation checker stop being prompt context and become the arbiter itself. The course: promote those assets from inputs to arbiter, delete the noise layer, make the LLM a proposer the model audits, keep the corpus as the model's calibration set (the fix diff is what the model should see), and defer execution to Clearwing for the memory-safety classes only. Build the arbiter we can build from code; adopt the one we cannot, when a class demands it. Co-Authored-By: Claude Opus 4.8 <[email protected]> Claude-Session: https://claude.ai/code/session_01T7XD7x5KonMdmGRkp63EQG |