Synthesis Review Bundles

modality model synthesize is review assistance. The rule remains the authority, and the model is only a witness that the current synthesis path found.

For parser-backed rules, ask the CLI to verify the witness and write a review bundle:

modality model synthesize \
  --rule rules/post-requires-reviewer.modality \
  --source-file source/post-requires-reviewer.txt \
  --verify \
  --review-bundle review/post-requires-reviewer.md \
  -o model/post-requires-reviewer.modality

A useful bundle should let a reviewer answer five questions before signing or committing the result:

• Which rule file was used?
• Which reviewer-authored source clause, prompt, or protocol text was preserved?
• Which action labels and predicate calls were extracted by the parser?
• Does the Source Facts section preserve any reviewer-supplied Source fact: lines such as concrete +sets(...) path-write expectations without treating them as automatically inferred facts, with source line numbers and shape labels such as path-write template for traceability?
• Does it flag malformed signed Source fact: shapes with review warning: malformed source fact instead of silently treating them as ordinary reviewer text?
• Does the Review Checklist say source capture, clause trace, parser-backed formulas, verifier result, assumptions, and known gaps are present?
• Does the Review Checklist summarize whether source facts were preserved, how many source facts were preserved, how many malformed source facts were flagged, how many path-write source facts were flagged, whether external assumptions were preserved, and how many external assumptions were preserved, plus how many commit-evidence, external-world, and reviewer assumptions were flagged?
• Does the Source Assumptions section preserve any reviewer-supplied External assumption: lines as out-of-proof evidence boundaries, with source line numbers and assumption-boundary labels for traceability?
• Does the Review Checklist say Prompt-to-facts trace: not automatic so the reviewer knows preserved source clauses still need human comparison against parser-backed formulas?
• Did --verify accept the witness model?
• Which assumptions and known gaps are still outside the proof?
• Does the witness model expose only the moves the rule intended?

Passing Bundle

For a rule such as:

rule post_requires_reviewer {
  formula {
    always([+POST -signed_by(/users/reviewer.id)] false)
  }
}

the bundle should include the rule source, extracted facts such as +POST and -signed_by(/users/reviewer.id), a Review Checklist with Verifier result: passed, Source facts preserved: yes, Malformed source facts flagged: 1, Path-write source facts flagged: 1, Source facts preserved count: 2, External assumptions preserved: yes, and External assumptions preserved count: 1, plus assumption label counts such as Commit evidence assumptions flagged: 1, External-world assumptions flagged: 0, and Reviewer assumptions flagged: 0, plus the witness model that the verifier accepted. Treat that witness as something to inspect, not as proof that the original human intent was complete.

When the rule came from reviewer-authored text, pass that text with --source-file or --source-text instead of relying on the rule file alone. Structured lines such as F1: Every accepted post move must have reviewer signature evidence attached. should appear in the Source Clause Trace section next to the extracted formula. This trace is preserved for review; it is not natural-language extraction. The Review Checklist should repeat that boundary with Prompt-to-facts trace: not automatic.

Structured lines such as Source fact: +sets(/posts/{post_id}/body) should appear in the Source Facts section. Use these for reviewer-supplied protocol or path-write facts that should remain visible next to the parser-backed formula summary. They are preserved with source line numbers and source-fact shape labels such as path-write template for review, but synthesis does not infer or prove them.

Malformed signed source facts, such as an unbalanced Source fact: +sets(/posts/{post_id}/body, should remain in the same section with a review warning: malformed source fact label. That warning means the line was preserved for audit, but reviewers should not treat it as structured path-write or predicate evidence until the source text is fixed.

Structured lines such as External assumption: signature verification and path identity evidence come from commit data. should appear in the Source Assumptions section with labels such as commit evidence boundary. Treat those lines as explicit review boundaries: synthesis preserves them, but does not prove them. External-world dependencies such as DNS control, HTTP control, CA policy, WebPKI trust, cryptographic soundness, payment settlement, or physical delivery should be labelled as external-world boundary.

No-Witness Bundle

If --verify rejects the synthesized candidate, the CLI should say that no satisfying witness was found by bounded μ-calculus search. With --review-bundle, it should still write a failed bundle containing:

• The rule file and parser-backed extracted facts.
• Any Source fact: lines supplied with the original source, or an explicit note that none were supplied. Supplied facts should include their source line numbers and source-fact shape labels, including malformed-source warnings.
• Any External assumption: lines supplied with the original source, or an explicit note that none were supplied. Supplied assumptions should include their source line numbers and assumption-boundary labels.
• A Review Checklist with Verifier result: failed, source-fact preservation, source-fact count, malformed-source-fact count, external-assumption preservation, path-write-source-fact count, external-assumption count, and assumption label counts.
• The verifier error.
• The candidate witness model that failed verification.
• Assumptions and known gaps, including the bounded explicit-state μ-calculus search.

This is not a contract approval. It is a review artifact that says the current tooling did not find a satisfying witness. Revise the rule, supply a witness model manually, or improve the synthesizer before treating the rule as ready.

Review failed bundles with the same care as passing bundles. The failure is useful only when it preserves enough evidence to diagnose the gap:

• Confirm the rule source is the text the reviewer intended to check.
• Compare extracted facts with the formula and look for missing labels or predicates.
• Read the verifier error before changing the rule; it may point at an unsupported synthesis pattern instead of an impossible contract.
• Inspect the candidate witness model to see which candidate the search tried.
• Keep the known gaps attached to the review record when the next revision is proposed.

For an intentionally impossible rule such as:

rule impossible_contract {
  formula {
    false
  }
}

a failed bundle should preserve the rule source, state that --verify failed, include the rejected candidate witness model, and name the bounded explicit-state μ-calculus search as a known gap. That is a useful negative result: it tells reviewers the tool found no current witness instead of quietly presenting a model as if it proved the rule.

Review Boundary

The current parser-backed path covers rule formulas and generated witness models. It does not automatically prove that natural-language intent, real-world evidence, or external predicates are complete. When a bundle mentions assumptions, keep them visible in the contract review instead of hiding them in the generated model.