RFC: spec extensions for qualified-tool bridge, formal-verification (proof) coverage, model-based-design traceability, and Ada/SPARK onboarding

[SoundMatt]

Context

Roadmap item covering both the "depth" and "Ada/SPARK breadth" tracks discussed 2026-07-27. This issue is the spec-design document — it defines the common JSON schemas and CLI conventions once, here, so the per-tool implementation issues (linked below) build the same wire format instead of three slightly-different ones. Follows the same pattern as the §1.4.1 requirement-annotation-completeness addition landed earlier today: spec RFC first, then per-tool adoption issues that reference it.

Companion implementation issues: SoundMatt/c-FuSa (TBD, added once filed), SoundMatt/cpp-FuSa (TBD, added once filed).

---

A. Qualified external tool bridge

Lets a project's existing LDRA/VectorCAST/Polyspace/Coverity investment feed into the same aggregated Finding stream as native x-FuSa findings, instead of being a second, disconnected source of truth.

<tool> check --import <path> --import-format ldra|vectorcast|polyspace|coverity|generic

• --import-format generic accepts a file already in the canonical Finding[] shape (spec §4) — the escape hatch for any external tool not yet natively supported.
• Each named format gets a decoder mapping the external tool's native report into Finding objects. Set tool to the external tool's lowercase name (e.g. "coverity"), not the x-FuSa tool's own name, so aggregated output can distinguish native vs. imported findings by tool while still normalizing severity to the canonical INFO/WARNING/ERROR enum (§2.4) via a per-format severity-mapping table (e.g. Coverity's Major/Moderate/Minor impact → ERROR/WARNING/INFO).
• ruleId = the external tool's own rule/checker ID verbatim (e.g. "MISRA_CAST"). Map to the §1.5.1 category-prefix table where the checker name matches a known prefix; otherwise category: "other".
• Imported findings MUST still receive a §4.2 fingerprint so they participate in diff/suppression identically to native findings.
• MVP scope: implement the coverity decoder first (cleanest JSON export of the four) — it exercises the --import/--import-format flag plumbing and the decoder-registry pattern the other three formats will reuse. Don't build all four at once.

B. Formal-verification (proof) coverage

A new canonical evidence type, modeled directly on the existing MC/DC pattern (McdcReport, --mcdc/--mcdc-file/--mcdc-threshold) — same shape of problem (external analysis tool produces structured coverage data, tool ingests it, FuSaOps aggregates cross-language), different metric (formal proof obligations discharged, not test-exercised conditions).

// proof-report.json
{
  "...envelope": "...",           // §3.1 common header
  "tool": "cbmc",                 // or "frama-c"; "gnatprove" once ada-FuSa exists
  "totalObligations": 240,
  "provedObligations": 231,
  "proofPct": 96.3,
  "gatePassed": false,
  "functions": [
    { "name": "compute_checksum", "file": "src/checksum.c", "totalObligations": 4, "provedObligations": 4, "proved": true },
    { "name": "parse_header",     "file": "src/parse.c",    "totalObligations": 6, "provedObligations": 3, "proved": false }
  ]
}

CLI convention (mirrors --mcdc/--mcdc-file/--mcdc-threshold exactly):

<tool> coverage --proof --proof-file <path> --proof-threshold N

• --proof-file points at the underlying prover's own native output (CBMC's --xml-ui, Frama-C's WP report, future gnatprove's .spark summary). Each tool parses its own prover's format but MUST emit the proof-report.json shape above.
• --proof-threshold N gates exactly like every other threshold flag in the spec: exit 1 when proofPct < N.
• FuSaOps side: new proof package (mirrors mcdc), fusaops proof cross-language roll-up command, dashboard section, /api/v1/proof endpoint — same shape as the existing MC/DC dashboard work.

C. Model-based-design (Simulink) traceability bridge

New canonical input file, dot-prefixed and un-tool-prefixed per the existing §1.2 convention (same tier as .fusa.json, .fusa-reqs.json):

// .fusa-model-trace.json
{
  "modelFile": "controller.slx",
  "links": [
    { "requirementId": "REQ-CTRL-014", "modelBlock": "Controller/PID/Saturation", "generatedFile": "src/pid_saturate.c", "generatedLine": 82 }
  ]
}

This file is produced by a documented (not our problem to build) conversion step from Simulink Requirements Toolbox's own CSV/XML export — the tool only ever consumes this JSON, never talks to MATLAB directly.

<tool> trace --model-trace .fusa-model-trace.json

merges each link into the existing trace matrix as a new tag kind "model", alongside the existing impl/test/sec-test (§1.4) — so a requirement can show [traced+tested+modeled].

D. Ada/SPARK — new ada-FuSa tool

Follows the identical onboarding process already used six times (docs/extending.md): full x-FuSa spec CLI surface, same JSON schemas, same annotation convention as Ada comments (-- fusa:req REQ-..., -- fusa:test REQ-...).

Two things make this more than "a 7th copy of the same tool":

1. SPARK proof coverage is ada-FuSa's flagship evidence type, using the Section B schema with tool: "gnatprove". This becomes the reference implementation that c-FuSa/cpp-FuSa's Frama-C/CBMC support should match bit-for-bit — build Section B first (against CBMC/Frama-C) so ada-FuSa isn't inventing the schema under time pressure later.
2. No established "MISRA-Ada" rule set exists. The coding-standard rule pack should draw from the Ada Quality and Style Guide rather than porting a MISRA-style numbered list — recommend a new ADA-<n> rule-id prefix alongside the existing MISRA-*/AUTOSAR-*/CERT-* convention in spec §1.5.1.

This issue does NOT create the ada-FuSa repository. That's a separate, more consequential action (a new public repo) requiring explicit confirmation before it happens — flagged here as the acknowledged prerequisite for Section D, not bundled into this RFC.

Sequencing recommendation

1. Section A (Coverity import) and Section B (CBMC proof coverage) on c-FuSa/cpp-FuSa — both are additive, low-risk, and Section B directly derisks the Ada work.
2. Section C (Simulink bridge) — needs the schema validated against a real Simulink Requirements Toolbox export before committing to the JSON shape above.
3. Section D (ada-FuSa) — once Section B's proof-coverage schema has shipped and proven itself in at least one existing tool.

[SoundMatt]

Companion implementation issues filed:

• feat: AUTOSAR Classic Platform C rule pack + Coverity import bridge + CBMC proof coverage c-FuSa#66 — AUTOSAR Classic Platform C + Coverity import + CBMC proof coverage
• feat: AUTOSAR C++14 Guidelines rule pack + Coverity import bridge + CBMC proof coverage cpp-FuSa#33 — AUTOSAR C++14 Guidelines + Coverity import + CBMC proof coverage

Both reference this issue for the common schemas (§A/§B) rather than re-deriving them. Section C (Simulink bridge) and Section D (ada-FuSa) remain design-only until the CBMC proof-coverage schema has shipped and proven itself in at least one of the two above.

[SoundMatt]

Formalized in #81, released as spec v1.12.0 (FuSaOps v1.137.0).

docs/x-fusa-spec.md now defines the canonical wire format for all four RFC sections, all additive draft/SHOULD entries — no tool implements any of them yet:

• §4.3 check --import/--import-format — qualified external tool bridge (Section A). generic format is the required baseline; coverity recommended as the first named decoder (MVP scope, per the RFC).
• coverage --proof (§9.2) — formal-verification/proof-obligation coverage (Section B), modeled on the existing MC/DC pattern. proof-report.json schema + --proof-file/--proof-threshold convention, tool: "gnatprove" reserved for a future Ada/SPARK tool.
• §1.2.4 .fusa-model-trace.json + §5 --model-trace/"model" tag kind — model-based-design bridge (Section C). Explicitly marked draft, pending validation against a real Simulink Requirements Toolbox export, per the RFC's own caveat.
• §1.5.1 ADA-<n> rule-id prefix (Section D) — Ada Quality and Style Guide-derived, alongside MISRA-*/AUTOSAR-*/CERT-*. (Note: ada-FuSa itself was already onboarded as the 7th adapter in FuSaOps v1.136.0, ahead of this RFC — this piece formalizes its rule-id convention retroactively.)
• §13 gained schema-status rows for all three new draft schemas; SpecVersion bumped 1.11.0 → 1.12.0.

Out of scope, as called out in the RFC and left for separate tracking: actual Coverity/CBMC implementation in c-FuSa/cpp-FuSa, and Section C's schema validation against a real Simulink export.

Closing as the spec-design deliverable is complete.