PR 3/3: Crucible backend by ericeil · Pull Request #98 · Certora/AutoProver

ericeil · 2026-07-23T18:43:16Z

PR 3 of 3 — Crucible backend (capstone)

Part of the stacked split of eric/crucible (see docs/pr-split-plan.md).
Stack: master → eric/ecosystem → eric/rust → eric/crucible-app.
Base: eric/rust (PR #97) — review PRs #96 and #97 first.

The tip of the stack — the Solana verification application, wiring PR 1 (ecosystem) +
PR 2 (rust framework) + the upstream command sandbox together.

What this adds

composer/crucible/* and rust/crucible-app (the Crucible wheel)
Crucible RAG: committed manifest rust/crucible-app/crucible_kb.rag.json + shared
composer/scripts/rag_import.py, composer/rag/{import_format,db}.py, composer/tools/crucible_rag.py
ReportBackend "crucible" + render labels + as_report_backend
Sandbox default → launcher for crucible (fail-closed; the launcher itself is upstream)
test_scenarios/solana_vault + the crucible test gates — the vault sample also makes PR 2's
test_solana_gate runnable from here
docs/application-abstraction.md — the five pieces of an analyzed application / Rust app
framework (moved here from the ecosystem PR, where it did not belong), plus the crucible-*
design docs

Finalizes the PR 2 cross-cutting intermediates

rust/Cargo.toml re-adds the crucible-app workspace member.
rustapp/adapter.py swaps the tag cast back to the validating as_report_backend, now that
report/schema.py closes ReportBackend to {prover, foundry, crucible}.
Carries the crucible-specific sandbox tweaks: sandbox/recipes.py per-run RUSTUP_HOME;
docker-compose.sandbox.yml un-gated run-confined-build.

Verification

cargo build (all 4 crates) ✓
crucible-layer modules import ✓

Notes

Draft: the real-LLM gates were not run here — test_crucible_gate,
test_crucible_setup_gate, test_crucible_formalize_gate, test_crucible_e2e_gate.
(setup/formalize were verified green earlier this cycle against a real crucible build.)

🤖 Generated with Claude Code

master had to generalize two docstrings when it dropped the solana_vault leftovers PR 97 leaked there: the scenario, tests/test_crucible_sandbox_gate.py, and the Crucible design notes are all on this branch, not on master, so naming them upstream left dangling paths. Here they resolve, and naming them is more useful than describing them. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>

master's plugin tool contribution (#158) gave Formalizer.formalize an `extra_tools` binder. The Rust backend accepts it without using it yet — as master's own RustFormalizer does — but two call sites here predate the parameter and died on the missing argument. Pass `cast(Any, None)`, the same placeholder the null-backend tests already use for a binder nothing reads. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>

The branch arrived with its own answer to "what did this run find" — a `FINDINGS.md` sidecar written from `finalize` — and the base it now sits on has the seam that answer was a stand-in for. The sidecar and its tests went with the rebase (docs/rust-applications.md §6 no longer describes them); what is left is reconciling the two sides that were written independently. **A section's finding is its own.** Crucible delivers one crate, so `validate` files each verdict under its section (`c_<slug>.rs`) — without it two authors given the same property title collapse into one report row. The findings mapper keys observations by the same `(file, name)`, and nothing until now exercised the two together. It does: two sections naming one check keep their own crash. **First component wins a collapsed key, as in `collect`.** Where two components do share a key — a callout-mode wheel that names no file — `collect` keeps the first run and the mapper kept the last, so a row's message and its finding's proof of concept could describe different runs. `tests/test_rustapp_declared_findings.py` is gone: every one of its eight tests is in `tests/test_rustapp_findings.py` under the same name, which is where the base folded them. Its klend narrative moves to that module's docstring. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>

Restores master's seam verbatim, ahead of extending it. `build_findings` returns to `composer/spec/source/report/findings.py`, `RuleEvidence` and `EvidenceFetcher` to `report/collect.py`, `findings_llm`/`fetch_evidence` to `build_report`, and `Formalizer.findings_evidence()` in place of `Formalizer.findings` / `FindingsBuilder`. The Rust mapper (`composer/rustapp/findings.py`) goes with it: it existed to submit ready `Finding`s through a hook that no longer exists, and what replaces it is the shared synthesizer parameterized for a fuzzer, in the commits after this one. Crucible therefore reports no findings between here and there. Kept, because they are this branch's and not the seam's: `expected_failures` and `reported_verdicts()` on `RustFormalResult`, and `display_name`. Those are what the console rollup and the verdict rows read, and the declaration fold is tested on its own in `tests/test_rustapp_findings.py`. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>

`build_findings` had one backend's answers baked into a shared function: evidence was `RuleEvidence` (label / analysis / counterexample), the prompt said the Certora Prover found a concrete counterexample, and severity came from the impact × likelihood the model was required to assess against it. A second backend could only join by pretending its evidence was the Prover's. The loop stays shared, because none of it is backend-specific: walk the BAD rules, resolve each one's properties and the audit groups they sit in, bound the concurrency, keep one failed write-up from costing the rest, compose the `Finding`. What varies moves onto a `FindingsSynthesis[E, D]` the backend returns — generic over its evidence and the draft it asks the model for, so neither is a union of every backend's needs. `assess` is the severity plus the record of how it was reached, so a backend whose evidence does not establish exploitability can return a constant instead of a rating nothing produced — rather than steering the matrix from prompt text. Evidence is keyed by `RuleRef` — `(file, name)` — not by rule name. That is how the report identifies a row, and a name alone does not: one deliverable can hold several components' checks, and two authors given the same property title write the same check name. The Prover's fetcher drops the file half and says why: `CexAnalysisStore` is name-keyed because a `RulePath` has no spec file on it, so two components whose specs share a rule name share evidence. Closing that needs the capture to carry the file; it is not this call's to fix. `Formalizer.findings_evidence()` becomes `findings_synthesis(outcomes)` — same opt-out by returning None, and it takes the outcomes because a backend whose evidence is in its own results has nowhere else to read it from. The Prover's half (evidence type, draft, templates, matrix) moves to `composer/spec/source/prover_findings.py`. Docs: formalization-abstraction.md §4.6. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>

Fills the seam the previous commit opened. A Rust backend now returns a `FindingsSynthesis` and its BAD rows reach `report.html`'s Findings section as written issues rather than not at all. **Evidence is `FuzzEvidence`, one per check**, keyed by `(file, name)` as the report keys its rows — which for Crucible means the section file, since one crate holds every component's checks and two authors given the same property title write the same check name. First component wins a collapsed key, as in `collect`, so a row's message and its finding's proof of concept are never from different runs. It keeps the wheel's *own* outcome apart from the author's declaration, which is the split `RuleEvidence` has nowhere to put. A declared check reports BAD either way, so only those two together say whether a reader is looking at a crash the fuzzer found or a claim the author made from reading the source — and a write-up that confuses them is worse than none. **The prompt says what that evidence is.** A fuzzer drove a harness the author wrote from a state that harness set up; the campaign's `SUSPECT HARNESS BUG` marker is the first thing a reader needs, an unreproduced declaration must not be handed a counterexample it does not have, and the harness caveats belong in `assumptions_and_uncertainties`. **Severity is `informational`, with the axes empty.** A campaign establishes that an assertion can be made to fail, not that anyone can profit from it: a crash on a failed precondition looks exactly like a crash on a real one. Assigning that a rating would be inventing one. `provenance.risk_reasoning` carries the author's declaration instead, where there is one. Not fixed here, and marked where it lives: `Verdict.detail` is the counterexample with the campaign accounting appended, and nothing host-side can tell where one ends — so the accounting is inside the proof of concept. Separating them is a wire change, not a parse. Docs: rust-applications.md §4.5. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>

`Verdict.detail` carried both: the campaign's counterexample, then whatever `tally::gate` and `campaign.rs` had to say about what the run covered and spent, appended behind a blank line. Nothing on the host could tell where one ended, so a Crucible finding's proof of concept read crash crash_e953: [authority_must_sign_initialization] … reproducing sequence (iteration 3, 3 action(s)): … [Vault Initialization] campaign spent 67798 executions in 597s of a 600s budget — a claim about the program and a claim about the run, presented as one piece of evidence. `Verdict` gains `accounting`, and the two producers of run accounting write there (`Verdict::noting` appends, because both contribute to one verdict). `detail` goes back to being only what the campaign observed: a counterexample, or the error behind a run that reached no verdict. Nothing visible is lost. `fetch_verdicts` rejoins the halves into the report row's one `message` — evidence first, since a BAD row's first line is what a reader is looking for — so a green row still says what it cost, which is the whole reason `campaign.rs` exists. The live console, which shows a detail's first line, now shows the counterexample or nothing rather than accounting on every green check. `FuzzEvidence` splits to match, and the findings prompt introduces the accounting as what it is: what the campaign covered, for `assumptions_and_uncertainties`, rather than more of the crash. Wire change, so the wheel needs a rebuild: uv sync --group test --group ci --group ragbuild --group apps \ --extra cpu --extra certora-cli Docs: rust-applications.md §§4.5, 6. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>

`build_findings` spent a heavy model per BAD row, which was fine while a row and a finding were the same thing. They are not for a fuzz campaign: one covers a component's whole property set, and `attribute_findings` condemns every check in it when a crash names a property no component in the run claims — because the counterexample is real and hiding it would be worse. On a klend-sized component that is 26 BAD rows of one crash, and per-row synthesis would buy 26 heavy-model calls publishing 26 accounts of it, each guessing a different check it might have been. `FindingsSynthesis.collapse` gives a row's *finding* an identity. Rows sharing one are written up once, against the first of them, with the rest on `FindingRequest.also_covers` — which the fuzz prompt uses to say the campaign found a violation it cannot place and to forbid pinning it on any one check. The Prover returns `rule.ref` and never collapses: its evidence is captured per rule, so no two rows can be the same finding. Crucible keys on the counterexample, which also handles the honest case — a crash naming two properties genuinely refutes both, and one write-up covering both is the right answer. Rows with no counterexample fall back to their own identity, so two declared findings the run did not reproduce stay two claims however alike the accounting behind them looks (it is the same campaign, so it is identical). Evidence is now fetched for every BAD row before any write-up, since the grouping needs it. A fetch that fails drops that row, as it did when it happened inside the write-up. Docs: formalization-abstraction.md §4.6, rust-applications.md §4.5. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>

`composer/rustapp` hosts any Rust wheel, but its findings synthesis was Crucible's: a system prompt about fuzzing campaigns and `SUSPECT HARNESS BUG`, a severity pinned to `informational`, and a collapse rule that recovered "these rows are one crash" by string-comparing counterexamples. `example-app` would have been written up as a fuzz campaign, and a wheel with real exploitability analysis could not have said so. Two declarations move to the wheel. `AppDescriptor.findings` carries a `FindingsPolicy`: the domain half of the write-up system prompt, and a `SeverityPolicy` of `Assessed` (the model rates impact and likelihood, host maps them through the matrix) or `Fixed { tier }` (no rating is asked for at all). It mirrors `Backend::judge` — wheel supplies the domain half, host appends the protocol half — and `None` means this wheel produces no findings, because a write-up asserts what its evidence is and a host that guessed would publish prose nothing stands behind. Crucible declares its campaign prose and `Fixed { informational }`; example-app declines. The severity policy also picks the schema, since ignoring an unsupported rating is not the same as not asking for one: `Fixed` gets `FindingDraft`, `Assessed` gets the new shared `AssessedFindingDraft` (the prover's three axis fields, reworded off "counterexample") with `assessed` as its `FindingsSynthesis.assess`. `Verdict.finding` carries which finding a verdict belongs to. `attribute_findings` already knows, at the line where it fans an unplaceable crash across a whole target, and was discarding it; the host then rebuilt the relation from payload text. Now the wheel stamps it and the host groups on the key. That is not just tidier: rows fanned out from one conclusion are indistinguishable from several checks that failed identically, and those are two different facts about the program, so only the producer can say which. What is left in `composer/rustapp/findings.py` reads wire fields only — `detail`, `accounting`, `finding`, the declared failures — and its prompt template is worded for a "run" rather than a campaign. Also drops a `mut` left stale by 2b998b1, where `Verdict::noting` became consuming. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>

The generic `E` on `FindingsSynthesis` was justified as keeping the prover's counterexample capture and a wheel's crash metadata from merging into a struct whose fields half-apply. Checked against the actual fields, that does not hold: `analysis`, `counterexample`, `label`, `ran`, `accounting` and `declared` are "instance, explanation, reproducer, and what the run itself did", which is not a claim about any one backend. Only the *vocabulary* was prover-shaped — master's `RuleEvidence` docstring talks about parametric bindings, and `CheckObservation` described `accounting` in fuzzing terms — and a field a backend cannot fill is exactly what optionality is for. Absence means "this run recorded nothing of that kind" for all of them, so a prompt can say what is missing rather than guess. `RuleEvidence` moves to `report/findings.py` and gains `ran`, `accounting`, `declared` and `finding`. `CheckObservation` is gone; the wheel host maps its verdicts straight into it, leaving `analysis` unset — a wheel reports what its run found, not a reading of why the check broke, and the prompt has to be able to tell a reader which it is holding. With one evidence type, two of the seam's hooks stop being backend answers: - `proof` -> `proof_of_concept`. The prover joins its instances' traces (labelled past one) and the wheel filtered on `ran is BAD`; one function does both, since "no separate run outcome" is a backend that only captures failures. The rule is now stated once and the rust prompt template shares it. - `collapse` -> `finding_key`. The prover's was `rule.ref`; the wheel's was the stamped key falling back to `rule.ref`. The prover stamps nothing, so these were the same function. The relation is still never inferred from the evidence. What is left is what genuinely differs: where evidence comes from, what the model is told it is, and whether the evidence can carry a risk judgement. `draft` and `assess` stay a pair for now, though they are not independent either — every construction site pairs `AssessedFindingDraft` with `assessed` or `FindingDraft` with a constant, and the wheel's own `SeverityPolicy` already models that as one choice before `rust_findings` expands it into two fields. No wire change: `Verdict.finding` already carries the stamp, so no wheel rebuild.

Three of the four remaining seam fields were behaviour only by accident. `prompt` was a callable per backend, but both implementations did nothing except rename fields on their way into `.bind()`: the prover's template reads `rule_name`/`instances` and the wheel's reads `check_name`/`observations`, over the same `FindingRequest`. Renamed both templates onto one shared `FindingsPromptParams` and let `build_findings` do the binding. The backend still owns the prose — which is the part that is genuinely its claim — and `FindingRequest` goes, since it was the params dict wearing a dataclass. `draft` and `assess` were one decision written twice. Every construction site paired `AssessedFindingDraft` with `assessed` or `FindingDraft` with a constant, and nothing could have paired them otherwise: `assess` can only read what came back, so the schema is what decides whether a rating can exist at all. They are now one `SeverityFrom` — `Assessed | Fixed(tier)` — with each variant carrying the draft it implies, so asking for axes and then ignoring them is unrepresentable. The wheel already modelled it this way on the wire; the host was expanding one declared choice into two independent-looking fields. Sharing `RuleEvidence` in the previous commit is what made `Fixed` possible without a callback: its `reasoning` reads `declared`, which used to be a wheel-only field. What is left is `fetch_evidence` (the only hook, and the only one that does I/O), `system`, `prompt`, `severity`. `FindingsSynthesis` stops being generic, so the `Any` at the `Formalizer` and `build_report` seams goes with it. Adds a test for the prompt binding. It is shared code now, and a deliberately empty bind passed the whole suite: the two prompt tests exercise their templates directly, so nothing covered the loop putting this run's evidence into them.

`FindingsSynthesis` stopped being a table of hooks two commits ago — it is four values, one of which happens to be a fetcher — so the name should stop describing an action. `FindingsPolicy` fits, and `Formalizer.findings_synthesis` follows it to `findings_policy`. That name was taken by the wheel's wire type, which is a different thing: two of the policy's four fields, declared by the wheel and read by the host. Renamed to `FindingsDeclaration` on both sides of the FFI, so the wheel *declares* and the host holds the *policy*. The Rust struct name is not on the wire — the JSON key is still `findings` and the fields are still `system`/`severity` — so this changes no wire format and needs no wheel rebuild. Mechanical apart from `rust_findings`, whose parameter was `policy` for the wire type and now reads `declared` against a `FindingsPolicy` return.

Drops fixed severity. `Assessed`/`Fixed`, the wire `SeverityPolicy`/`SeverityTier`, the two draft schemas and the branch in Crucible's system template all go; there is one `FindingDraft` carrying the axes, and `severity_for`'s matrix maps them for everyone. `FindingsPolicy` is down to three fields and `FindingsDeclaration` to one. This changes what a Crucible finding asserts, not just how it is built. Its severity is now a model's exploitability rating derived from a crash that establishes an assertion can be made to fail and nothing more. Two things move with it: - `provenance.impact`/`likelihood` are always populated, so "nothing assessed this" is no longer distinguishable from an assessed `none` — which means "no real-world exploit path", a judgement about the program. - `provenance.risk_reasoning` is the model's justification, not the author's `expect_check_failure` reason. That reason still reaches the prompt, so a write-up can use it, but it is no longer recorded as the ground for the tier. The whole weight therefore falls on the declared prose, and Crucible's now says what its evidence does *not* establish rather than relying on a fixed tier to say it. The comment on `crucible-app`'s declaration says the same. Wire change (`findings` loses `severity`), so the wheel is rebuilt. Round-trip and descriptor tests confirm the installed wheel matches. Tests follow the reversal rather than being deleted: `test_a_fuzz_finding_carries_no_risk_rating` becomes `test_a_fuzz_finding_is_rated_like_any_other` and asserts the axes reach provenance and the matrix maps them; the two-declarations test discriminates on the prompts, since risk_reasoning no longer carries the author's text; the two policy tests collapse into one.

The rust system template was never rust-specific: `{{ domain }}` plus a WHAT TO PRODUCE block that names no backend. The CVL prompt is the same two halves fused into one static file — a domain claim (the Prover refuted this with a counterexample, treat it as confirmed) wrapped around a contract (the severity bands, the grounding rule) that says nothing about CVL. Split it the same way. `autoprove_report_findings_system.j2` is now the shared contract taking `{{ domain }}`, and the Prover's half moved to `autoprove_report_findings_prover_domain.j2` beside Crucible's, which lives in the wheel. Both backends render through one template. The host does the wrapping, for the same reason it binds the prompt: `FindingsPolicy` carries `domain`, and `build_findings` renders the message once per run. So a backend supplies two pieces of prose and no rendering, and the wire field follows — `FindingsDeclaration.system` is now `domain`, since it never was the system message. Two prompt changes fall out, neither purely mechanical: - Crucible gains the severity bands and the "report computes the tier from your two axes" line. It had neither; its model saw the bands only through the draft schema's field descriptions. This matters more since fixed severity went away. - CVL gains the `impact` / `attack_path` / title guidance the rust contract carried, and its band wording loses "counterexample" so it reads for both. The bands are still stated twice — here and in `FindingDraft`'s field descriptions. That predates this change for CVL; collapsing it is a prompt-quality question that wants an expensive run to answer, not a refactor. Wire change, so the wheel is rebuilt. `_CountingModel` now keeps the system message as well as the prompt, and the wheel-prose test goes through the real loop — the wrapping is host-side now, so asserting on the policy alone would no longer reach it.

`_RUST_PROMPT` named the backend the module already is, not the template. Both backends now hold the same seam field, so name both handles after what they render: the per-rule write-up prompt. The manifest keys on qualname, so it moves with the rename.

Both types were master's, in `report/collect.py`; this branch moved them to `report/findings.py` while widening them. Moving them back puts the widening where it reads as a widening: the diff against master is now the added fields and the re-keyed fetcher, not a file-to-file move. Consumers import from `collect` as they do on master, rather than through `findings` re-exporting what it imports.

`family_param` binds its name to a `_TemplatedTool` wrapper, while `with_template` instantiates a subclass of the *wrapped* class — so the class the decorator names is never the class the tool produces, and `family_param`'s `type[T]` return annotation hides that from the type checker. With state annotated as the wrapper, the first `map_checks` poisoned it: every later tool taking the injected state failed validation under `loc=('state', ...)`, which langgraph strips as an injected argument, so the model received an empty error string, retried against it forever, and the session gave up. Every Crucible authoring session has done this since #170. Keep the plain model for state and give the tool a templated subclass of it, whose instances state therefore accepts. Its schema title is pinned, since templating takes that from the class name and it is prompt text. The guard drives the real tool: constructing a `PropertyCheckMapping` directly, as the existing tests do, builds the class state names rather than the one the tool produces, which is why none of them saw this. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>

Deselected from the routine pass, these had rotted against the APIs they drive: `build_source_tools` grew an `ecosystem` parameter, `run_session` lost `checks`, and `crate_root` may answer `None`, which `parse_files` cannot take. The e2e gate also built its own confinement policy beside the entry point's, passing `sandbox_grants("{}")` — an argument `AppArgs` now rejects. It read `extra_ro` off the error envelope with `.get`, so the crucible repo was never granted, and preflight failed to load `crucible-fuzzer`'s manifest under the sandbox. Call the entry point's `build_confinement` instead, so there is one policy rather than a copy that can drift. The recursion limit these pass is the production default now: at 100 an authoring session ran out of graph steps mid-authoring, roughly 35 tool calls in. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>

Unpinned, `anchor idl build` resolves the release recommended for the program's anchor-lang and switches to it through `agave-install`, which writes ~/.config/solana — denied under the command sandbox, so no IDL is produced and the run fails with "no IDL could be produced". Pinning to the release already active makes the switch a no-op. A machine on a different release must change this line or supply --program-idl. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>

The checkpoint serializer restores a model by importing its class, and templating builds that class at runtime, so the templated instances `map_checks` was handing to `tool_state_update` came back from a checkpoint as bare dicts — and `run_session` read `m.property_title` off them as it assembled the session's result. Nothing reached that line while the tools were failing; with them working, every component died there instead. Build the declared `PropertyCheckMapping`, as `record_skip` already does for its own `SkippedProperty`. The guard now carries the mapping through the serializer too. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>

A long authoring turn (Opus thinking over a large prompt) can exceed the SDK's 600s non-streaming ceiling, and `timeout=None` explicitly DISABLES the SDK's timeouts (an explicit None is not not-given), so a socket that died silently mid-call hung the session forever — both observed on Crucible solana_vault runs. Stream every request so bytes keep flowing (no ceiling, no idle window for NAT killers to hit), and bound each httpx phase at 300s so a dead socket surfaces in minutes; for a streamed response that bounds the silence between chunks, not the whole turn. Co-Authored-By: Claude Fable 5 <noreply@anthropic.com> (cherry picked from commit 3578d3e)

A Crucible campaign reports one crash per violating input, so a check that is easy to violate gets one per input the fuzzer ever tried. A klend refresh-staleness check produced 7,166 crash reproductions; `validate_spec` spliced all of them into its tool result, which came to 5 MB / ~1.25M tokens and blew the context window outright: prompt is too long: 3181175 tokens > 1000000 maximum The component was lost with it — 26 properties, ~25 minutes of authoring — and nothing about the failure named the check that caused it. Bound the two seams where a verdict's `detail` becomes text a *model* reads: the validation tool result the author works from, and the evidence a findings write-up quotes. Both keep the head, where the wheel puts the deciding evidence, and say what was left out. The report path is untouched and still renders `detail` whole, so no evidence a reader can reach is lost. The bound lives on the wire `Verdict` because that is where the field lives, and because both consumers hold a `Verdict` rather than a bare string. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>

`cli_pipeline` installs a run-wide retry floor so a transient provider failure resumes that graph from its last checkpoint. `rust_entry_point` builds its own services and never installed one, so every graph in a Crucible run had `attempts = 1`: the first 500 anywhere in a component discarded however long it had been authoring. On klend that cost two components at ~2h each, and the run logged zero retries across five hours. The predicate already classified a 500 as retryable — nothing was asking it. Also classify `httpx.TimeoutException`. We stream now, and both the SDK's retries and its exception wrapping cover the *request*: once it has handed the response stream to the caller, a provider that goes quiet surfaces raw from the transport as `httpx.ReadTimeout`, which is what killed the second component. The floor's machinery is `test_graph_retry.py`'s subject; what is new here is the classification, so that is what the added test pins. The one-line install mirrors `cli_pipeline` and is not separately covered — exercising it means standing up the whole services stack. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>

The findings block said "rule <name> in <file>" for every backend. `ReportTerms` exists so the page reads correctly for each one — the rest of the template goes through it — but this line was a literal, so a Crucible fuzzing report announced its counterexamples as violations of "rules", a word that belongs to CVL and names nothing in a fuzzing campaign. `unit_singular` is the wrong term to reach for here: for the prover the two coincide (a rule is both the unit and the artifact), but Crucible's unit is a *property* and the thing that carries it is a `c_`-prefixed *check*, many-to-many with properties. Calling that a property would trade a foreign word for a wrong one. So this is a new term — "rule" / "test" / "check" — named after the neutral internal one, as `CheckVocab` is on the authoring side. The view-model field is renamed with it: it held a check name under the name `rule_name`. `FindingProvenance.rule_name` — the persisted schema — keeps its name; report.json is a serialized format with other consumers. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>

Every `terms.unit_*` slot labels the *rules*: the `total_rules` counts in the subtitle and footer, the chip label over `rule_counts`, and the verdict table whose rows are `c_`-prefixed check names. Crucible's entry filled all of them with "property", which is a different thing in this backend — the English claim the check carries, many-to-one with checks — and which the report counts separately right beside it. The subtitle read: 235 properties · 235 properties · 1 high-level properties Two counts of different things, in the same word. So this is what 7c4b2c0 should have been. It read the collision at the findings line as a missing term and added `check_singular` next to `unit_singular`; the values in `unit_*` were simply wrong, and one term was always enough. Dropped it again — every backend's `unit_singular` is now the word that line wanted. `none` keeps "property": it records properties without verifying them, so its rows really are properties and it has no check concept to name. Also pluralize the group count, visible in the same line at one group. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>

A component's checks share one campaign, and the campaign's exploration is shaped by whichever check is refuted first — so a sibling's GOOD is not its own evidence. Measured on klend: 35x the executions surfaced no additional check, and all 8 crashes were the same one. Writes up what the real fix looks like: make the check individually addressable (one authored fn per check), and let the host pick target granularity the way it already picks Exploration — grouped while the author iterates, per-check for the run whose verdicts reach the report. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>

Drops the Granularity idea from the proposal. Two grains would mean two truths: the author would iterate against the contaminated grouped verdicts the proposal exists to remove, and only the stamping run would be per-check — so a check green throughout authoring could flip at the gate. It also saved less than it looked, since the component feature has to exist anyway to seed corpora. The authoring cost it was meant to buy off is handled by a short Feedback budget and by focused validates, which per-check targets make real for the first time. Also renames Exploration to Stakes and takes the budget back off the seam. Exploration has one consumer, its two values are Crucible's two CLI modes, and the host already computes the only bit it knows (`partial`) before translating it into a fuzzer verb. A symbolic prover has nothing to do with "explore every covered check to the full budget" — it does not explore, and an unrefuted rule is a positive claim, not a budget-relative absence. `fuzz_timeout` is the wheel's own declared arg, so the wheel derives its budget from that plus the one bit. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>

A component was one campaign covering all of its checks, and the campaign's exploration was shaped by whichever check it refuted first: an input stops at its first violation and then leaves the corpus, so the states reachable past that check are reachable for none of its siblings — which are nonetheless reported GOOD. Measured on klend: 35x the executions surfaced no additional check, and all 8 crashes were the same one. `Exploration::ToBudget` promises "every covered check explored to the full budget"; this is what makes the wheel able to keep it. `target_for` now answers None — the seam's own spelling of "its own target" — so the host needs no change. What made that possible is the authoring contract: a section holds one `pub fn` per check instead of one fn holding every assertion, so a subset of a component is addressable at all. A component becomes a module rather than a build target, and its `mod` is gated on the union of its checks' features. The crate root can still be written before anything is authored, because targets are named from the run's *properties* — known then — rather than from checks, which are declared later. `CrateRootInput` gains that property set so the hook re-emits byte-identically what the setup gate rendered. The names are given to the author per property rather than derived by them. The prompt used to ask for `c_<property title>`, which equals the host's slug only when a title is already an identifier; harmless when a component was one target, a build failure when a check is one. `triage::unbuildable` refuses a target whose name is not one the root declared, before a build is spent, naming the expected one. Also renames Exploration to Stakes and takes the fuzzing budget off the seam; docs/per-check-targets.md §3 has the cost, §9 what the plan got wrong. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>

…identity The mapping was split in two — one class for the tool argument, an identical one for the state — because a `family_param` rendering was not an instance of the name the decorator bound. A value `map_checks` built therefore failed validation wherever state was annotated with that name, and failed invisibly: langgraph strips an injected-state error, so the model got an empty string and retried against it until the session died. graphcore#35 fixes that at the seam. A rendering now derives from the bound class, and `as_tool` / `tool_state_update` rebind a rendered value to it before it reaches state. So the split collapses to one class, the `ConfigDict(title=...)` that kept the split invisible to the model goes with it, and `run` no longer rebuilds what the framework already hands it. A test pins what the pinned title used to protect: the nested schema the model reads is named plainly and carries no unrendered placeholder. The pin names a commit on that PR's branch, not master; it moves again when it merges. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>

ericeil force-pushed the eric/rust branch from 0b7bb90 to a44644b Compare July 23, 2026 18:50

ericeil force-pushed the eric/crucible-app branch 2 times, most recently from bb347ed to f003b03 Compare July 23, 2026 19:46

ericeil force-pushed the eric/rust branch from a44644b to 4bbeb08 Compare July 23, 2026 19:46

ericeil force-pushed the eric/crucible-app branch 2 times, most recently from a707702 to d890343 Compare July 23, 2026 19:58

ericeil force-pushed the eric/rust branch from 7ea1a77 to 9a670d1 Compare July 23, 2026 20:15

ericeil force-pushed the eric/crucible-app branch from d890343 to a985a45 Compare July 23, 2026 20:15

ericeil force-pushed the eric/rust branch from 9a670d1 to a077199 Compare July 23, 2026 22:18

ericeil force-pushed the eric/crucible-app branch from a985a45 to c4f8b82 Compare July 23, 2026 22:23

ericeil force-pushed the eric/rust branch from a077199 to 4a1ecda Compare July 23, 2026 22:36

ericeil force-pushed the eric/crucible-app branch 2 times, most recently from 0712081 to 85b3424 Compare July 23, 2026 23:55

ericeil force-pushed the eric/rust branch from 4a1ecda to 75b0bec Compare July 23, 2026 23:55

ericeil force-pushed the eric/crucible-app branch from 85b3424 to f1381ae Compare July 24, 2026 00:02

ericeil force-pushed the eric/rust branch from 75b0bec to 0671f74 Compare July 24, 2026 00:02

ericeil force-pushed the eric/crucible-app branch from f1381ae to 18ba037 Compare July 24, 2026 00:08

ericeil force-pushed the eric/rust branch from 0671f74 to 5361ead Compare July 24, 2026 00:08

ericeil force-pushed the eric/rust branch from 5361ead to 37277ad Compare July 31, 2026 04:07

ericeil force-pushed the eric/crucible-app branch 3 times, most recently from e2249eb to e369524 Compare July 31, 2026 23:55

ericeil force-pushed the eric/rust branch from ee74e24 to 372504a Compare August 3, 2026 21:30

ericeil force-pushed the eric/crucible-app branch from e369524 to b4a6919 Compare August 3, 2026 21:30

ericeil force-pushed the eric/rust branch from 372504a to 65e2043 Compare August 4, 2026 18:35

ericeil force-pushed the eric/crucible-app branch 5 times, most recently from f47972f to e3a5925 Compare August 10, 2026 22:35

ericeil and others added 16 commits August 19, 2026 10:20

ericeil force-pushed the eric/crucible-app branch from 9a12bc4 to 13dc9d9 Compare August 19, 2026 21:30

ericeil and others added 13 commits August 19, 2026 16:30

Navigation Menu

Uh oh!

PR 3/3: Crucible backend - #98

PR 3/3: Crucible backend#98
ericeil wants to merge 86 commits into
masterfrom
eric/crucible-app

ericeil commented Jul 23, 2026 •

edited

Loading

Uh oh!

Reviewers

Assignees

Labels

Projects

Milestone

Development

Uh oh!

2 participants

Uh oh!

Conversation

ericeil commented Jul 23, 2026 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

PR 3 of 3 — Crucible backend (capstone)

What this adds

Finalizes the PR 2 cross-cutting intermediates

Verification

Notes

Uh oh!

Reviewers

Assignees

Labels

Projects

Milestone

Development

Uh oh!

2 participants

ericeil commented Jul 23, 2026 •

edited

Loading