Repository navigation
--export-json: a failed, empty, or partial run can serialize as a clean pass #4731
Description
--export-json is a -Z-gated, currently-undocumented output. Using it as a CI pass/fail
oracle in a standard-library verification effort, we hit several cases where the exported file
does not faithfully represent the run: a run that failed, was skipped, matched nothing, or
wasn't fully measured can be read as a clean, complete pass by a consumer that trusts the file.
These are reporting-fidelity issues in an unstable output — none changes a verification
verdict, a property status, or Kani's exit code. Grouped below by how each is best fixed.
Driver bugs — pre-existing (predate #4472), surfaced but not caused by --export-json; tracked as two small standalone PRs
A. A filter that matches zero harnesses runs to a completed / 0 failed export.
determine_targets only bails on a missing filter under --exact (metadata.rs:112); the
generic "no harnesses matched" bail lives in print_final_summary (harness_runner.rs:302),
which runs after the export is written — so a filter typo yields Ok([]), a clean-looking
export, and exit 0. Same area, independent of --export-json: print_final_summary
early-returns under --quiet (harness_runner.rs:255) before that bail, so
kani --quiet --harness <typo> skips the "no harnesses matched" error and exits 0.
Fix in determine_targets, before codegen and before any export.
B. --fail-fast drops the harnesses it skipped (#4729).
Root cause: collect::<Result<Vec<_>>>() (harness_runner.rs:105) short-circuits on the first
Err and discards already-completed Ok results. The lost harnesses are then absent from the
per-harness details, and the plain-text summary and SARIF under-report too — not only the JSON.
Fix the collect (#4729), not the reporter.
Deferred to RFC #4727
- Stale export is never invalidated. A run that reuses an existing
--export-jsonpath and
dies before the write leaves the previous complete-looking file in place. The completeness
mechanism (atomic temp-file + rename, "file exists ⇒ complete") is a schema/design decision
specified in RFC RFC: Structured verification results (export-json) #4727, not a writer patch. - No leaf-value / semantic validation of the exported file. Pending the RFC's open question
on shipping a JSON Schema (schemars) vs. a homegrown validator. cbmc_statsparsing is brittle (exactstrip_prefix/strip_suffix; a malformed duplicate
can clobber a valid value; overflow/absence collapse tonull). Pending the RFC decision on
whether CBMC statistics remain in the schema at all.
Schema (with the RFC)
harness_id == pretty_namecan misattribute across a workspace.pretty_namecan collide
between two crates, so the metadata↔details join can attribute a result to the wrong harness
(confirmed with a workspace carrying duplicate harness names). Fix: makeharness_id
crate-qualified (mangled_name/crate::pretty) — the consumer-facing id, not only the join.
The paired implementation PR #4732 is closed in favor of this decomposition: the two driver PRs,
the RFC, and crate-qualified harness_id.
Activity
feliperodri commentedon Aug 13, 2026
@ivmat I verified five of the six claims directly:
verify_project(main.rs:143) has a singlehandler.export()?at the end. Nothing invalidates the target first. True.determine_targetsonly bails when--exact(metadata.rs:112). The generic "no harnesses matched" bail lives inprint_final_summary(harness_runner.rs:302), which runs after the export. True.--fail-fastdrops skipped harnesses —process_harness_results(schema_utils.rs:336) hasif let Some(result) = ...with no else. True.*field = value.strip_suffix('s').and_then(...)assigns unconditionally (call_cbmc.rs:161). A later malformed duplicate erases a valid value. True. u32 overflow → null also true.pretty_namecollisions —pretty_nameisreadable_name, which strips the local crate prefix, so two workspace crates can share one. Real, though it needs a workspace with duplicate harness names.But labeling these [S] soundness is wrong, and that framing is doing a lot of work in the issue. None of them affect a verification verdict, a property status, or Kani's exit code. They are reporting-fidelity bugs in a -Z unstable-options-gated flag that has zero documentation (grep -rn export-json docs/src/ → nothing) and, as far as I can tell, one consumer: the reporter's own verified-std effort. "Soundness/misreport" reads like a CBMC-level unsoundness claim. It isn't.
feliperodri commentedon Aug 13, 2026
Also, @ivmat. Two of the six items are work against code the RFC #4727 deletes...
--export-jsonreporting a failed, skipped, or zero-match run as clean #4732 then buildsparse_leading_number_with_remainderto make that pattern-matching more robust.--export-jsonfor structured verification results #4472 on the grounds that "anything homegrown I write here gets thrown away when that's settled," pending the schemars/JSON Schema decision that is open question Consider having our own CBMC mode instead of just using "C" #1 in the RFC.feliperodri commentedon Aug 13, 2026
Let's be more concrete, @ivmat:
--quiet exit-0bug), and--fail-fastdiscards results for harnesses that already completed #4729. Both make issue items 2 and 3 disappear.harness_idcrate-qualified in the schema; the join-only change is cosmetic.The core a general user needs is per-harness status, per-property status/location/class, the exhaustive counts, and enough provenance to reproduce. The rest of what #4472 shipped is niche: CBMC internal statistics (VCC counts, symex time, slicing),
os_info,object_bits, and solver-binary version probing...create_tool_versions_jsonspawns a process per tool, andcbmc --versiontwice per run sinceget_cbmc_infoprobes it again. That's the surface generating the follow-up stream. Cutting v1 to the core, removes items 4, 5 and most of the schema-validator burden by construction.feliperodri commentedon Aug 13, 2026
Item 7 was filed unverified ("NEEDS CONFIRMATION"), which shouldn't be in an issue.
ivmat commentedon Aug 14, 2026
@feliperodri you are correct — this issue report and related PR were reported hastily without much thinking or consideration from my side. i wanted to "get on with it so I can add PRs on enhancements" but wanted to clear issues beforehand - and did not actually do disciplined work myself. the s labels overclaimed — you are right these are reporting-fidelity bugs, not soundness — and item 7 should not have been filed unverified. i apologise for causing unnecessary work for you and for wasting CI. you are taking time to do proper review so i should do the proper work myself
what i did now: close #4732 and edited this issue per your plan (removed s labels, dropped item 7, restructured per your comments). to be done: the 2 small kani-driver PRs first (zeromatch/quiet in determine_targets, and #4729). will reproduce both on my machine before writing any fix. items 4-5 wait for the RFC decisions, item 6 goes with crate-qualified harness id. ive done too much bulk-things — rigor and focus is what is most important & whats missing in general when using ai (especially for formal verification tool contribution delivery) and this clashes with my "get things out asap" approach.
Fail a zero-match harness filter before codegen and export (model-che…
RFC 0015: second fix pass from cold-panel synthesis
RFC 0015: cut v1 to the core — drop tools.solvers[]/aux tool versions…
RFC: Structured verification results (export-json) (model-checking#4727)
ivmat commentedon Sep 28, 2026
to summarize, all items from this issue are followed up:
A filter that matches zero harnesses → #4743 (merged): the filter now fails before codegen and before any export.
--quiet skips the failure exit code (#4745) → #4771 (open, in review).
--fail-fast drops completed results (#4729) → #4744 (merged).
Moved to RFC 0015
Stale export never invalidated → the RFC's completeness rules: temp file + atomic rename, and an INCOMPLETE marker once verification starts ("marker or delete-up-front" is still an open question).
No leaf-value validation → open question "JSON Schema document?" (schemars).
Brittle cbmc_stats parsing → CBMC statistics are excluded from the v1 schema (see "Why is CBMC statistics data excluded?"); restoring them is listed under "Dropped/transformed shipped fields?".
harness_id == pretty_name collisions across a workspace → harnesses[].crate_name; consumers join on (crate_name, name).