[devin-ai-integration]

What and why

A solver's verdict rests on two kinds of note the REPL already printed (%check, %solve, %explain, %configure, %optimize): the features the question reads as one value or object while only the default 0..* multiplicity governs them (Assuming X holds one value: it declares no multiplicity, so the default [0..*] governs it, recorded as Query.AssumedOne since #1553), and the object-holding features whose own assertions the question does not state (Query.Uncovered). The gRPC Verdict had no field for them, so the assumption behind a verdict was invisible to gRPC, MCP and every client. An assumption behind a verification verdict must be visible on every surface.

• One source of truth. solve.Note (Kind, Subject, Text) and Query.Notes() word each note once, in report order (uncovered first, then assumed). The REPL's noteLines prints Text from that list; nothing is re-formatted downstream. The REPL text of the uncovered note loses its REPL-only remedy (%instantiate and %validate → instantiate and validate an object to check it) so the same sentence reads on every surface.
• Protobuf. Verdict.notes = 18 (repeated VerdictNote), VerdictNote { kind = 1; subject = 2; text = 3 }, with kind ∈ assumed_one | uncovered. Stubs regenerated with make proto (Go, Python, TypeScript, Rust, descriptor); make proto-lint passes; JSON spells notes/kind/subject/text. Java message classes are generated by Maven, as before.
• Service. symbolicVerdict (the one path every solver-answered verdict of VerifyConstraint, VerifyRequirement and VerifySatisfaction goes through) fills Notes from the queries before asking the solvers, so an undecided solver answer still says what the translation assumed; an evaluation (question empty/evaluate) and a refused translation carry none. New verdict_notes capability (response-populated, like verification_verdicts), appended last; MCP server_info maps it to verify_constraint.
• MCP. verdictText prints each note under the verdict, as the REPL does.
• Clients. Go (Verdict.Notes, VerdictNote, NoteAssumedOne/NoteUncovered), Python (Verdict.notes, VerdictNote, NOTE_*, CAPABILITY_VERDICT_NOTES), Node (notes on every SysMLVerdict arm, VerdictNote, CAPABILITY_VERDICT_NOTES), Rust (Verdict.notes, VerdictNote, NOTE_*, CAPABILITY_VERDICT_NOTES), Java (Verdict.notes(), VerdictNote record, Capabilities.VERDICT_NOTES; the conformance renderer carries them back), Julia (Verdict.notes, VerdictNote, CAPABILITY_VERDICT_NOTES), MATLAB (Verdict.notes, capabilities().verdictNotes). The Go package conformance adapter carries notes back to the wire.
• Docs. docs/reference/api.md Verdict section, docs/reference/service-transports.md capability table, the compliance page (the multiplicity row now says the assumption reaches every gRPC verdict, a new row covers the notes on every surface, and the clients paragraph lists notes), each client's reference page, tests/grpc/testdata/conformance/README.md. Changelog fragment changes/unreleased/verdict-notes.fixed.md.

Specification basis

KerML 1.1 Beta 2 §7.4.12 (a feature that declares and inherits no multiplicity has the default 0..*) and SysML v2.1 Beta 2 §7.6.3 (the implicit [1..1] belongs to an eligible usage only — a bare in x : Real parameter is a reference usage and keeps the default), as #1553 established. This PR changes no semantics: it carries the assumption the solver already records to the transport. docs/project/spec-compliance.md: the "feature read as one value" row's text and implementation column are updated and one row is added after the verification-questions row (🧩 Extension); no row changes status. No oracle baseline moved.

How it was verified

Tests added:

• internal/frontend/grpc/verify_notes_test.go: a KerML feature level : Real read by an inv answers holds → violated with exactly one assumed_one note (subject Tanks::Tank::level, the REPL's sentence); the evaluation of the same constraint carries none; verdictNotes keeps the query order (uncovered, then assumed) over several queries.
• internal/frontend/grpc/robustness_verdict_notes_test.go (TestGRPCRobustnessVerdictNotes): an old client — the Verdict descriptor rebuilt without field 18 and VerdictNote — decodes a new verdict with the notes discarded and status intact; protojson spells the notes in camelCase and round-trips; a refused translation (**) is undecided with no notes.
• tests/grpc/testdata/conformance/verify_constraint_default_multiplicity.{sysml,expected.json} with a new VerifyConstraint RPC in the conformance runner (question, expected_status, expected_notes; skips without an SMT solver unless OPENSYSML_REQUIRE_SMT).
• internal/frontend/mcp/runtimetools/runtimetools_test.go:TestVerificationToolsPrintTheVerdictNotes.
• internal/frontend/grpc/capability_test.go: verdict_notes is the newest capability.
• Mirror tests per client (assumption note, uncovered note, no notes): Python tests/test_verification_questions.py, Node test/verify.test.ts, Rust results.rs unit tests, Java ResultProtosTest, Julia test/extended_client.jl ("verdict notes"), MATLAB tests/test_surface_offline.m.
• internal/frontend/repl/configure_nested_test.go: the three uncovered-note expectations follow the reworded sentence.

Gates run locally (z3 and cvc5 installed, so the solver tests ran rather than skipped):

• go build ./..., go vet ./..., gofmt -l . (empty), make proto + make proto-lint.
• go test ./... with OPENSYSML_REQUIRE_TRAINING_CORPUS=1 OPENSYSML_REQUIRE_PILOT_CORPORA=1 OPENSYSML_REQUIRE_SPEC_EXAMPLES=1 OPENSYSML_REQUIRE_SMT=1 after fetching the corpora: every package ok — 118 packages in the first run; cmd/sysml, internal/exec/runtime, internal/exec/smt and tests/codegen hit Go's 10-minute default under the parallel client suites and passed on a solo rerun with -timeout 60m (453 s, 338 s, 321 s, 492 s). make lint (staticcheck + gosec) passes; go test -C tools ./cmd/conformance/... covers the Go package conformance adapter.
• python3 scripts/changelog.py check, mkdocs build --strict.
• Clients: Python pytest tests/test_verification_questions.py (10 passed, 10 skipped: no live service); Node npm test against a fresh bin/sysml-grpc (454 tests, 453 pass, 1 skipped, 0 fail); Rust cargo test -p opensysml --lib results::tests (16 passed) and cargo check --all-targets; Java mvn -pl opensysml-client test -Dtest=ResultProtosTest,ResultTypesTest (37 tests, 0 failures) and test-compile of the conformance module; Julia test/runtests.jl (exit 0, verdict notes | 5 5). MATLAB is not installed here: Verdict.m and the offline test were checked by reading only.
• Dry-merge in detached worktrees: against origin/develop (f232fc5) and against chore(pilot): pin the OMG pilot implementation to release 2026-09 (0.63.0) #1529's head (9ca600a, chore/pilot-pin-2026-09) — both merge clean; on the chore(pilot): pin the OMG pilot implementation to release 2026-09 (0.63.0) #1529 merged tree go test ./internal/frontend/grpc ./tests/grpc ./internal/exec/solve ./internal/frontend/repl passes. chore(pilot): pin the OMG pilot implementation to release 2026-09 (0.63.0) #1529 and this PR share only docs/project/spec-compliance.md, in different rows. fix(solve): read a feature's multiplicity as the model computes it, assuming one value only where the default 0..* governs #1553 and fix(runtime): judge a behavior's write count by the feature's effective multiplicity #1556 are already in develop.

Not verified: the MATLAB suite (no MATLAB on this machine); a live Python/Julia run against the new service beyond the fake-transport mirror tests (the Go tests/grpc conformance case and the MCP test cover the service side).

Checklist

• make test and make lint pass locally
• Tests added or updated for the change
• Documentation extended where it already covers the surface (see CONTRIBUTING.md)
• Changelog entry added as changes/unreleased/<slug>.<section>.md, not as an edit to CHANGELOG.md
• baselines regenerated and make docs-counts run if a gate count moved (compliance rows need nothing: the census is counted at docs build)
• No internal work-item labels (waves, slices, F4, K5) in the body, docs, or changelog

Link to Devin session: https://nasa-jpl-demo.devinenterprise.com/sessions/c07151afb1e540a78ec7f5fb70824aaf
Open in Devin Desktop: https://nasa-jpl-demo.devinenterprise.com/desktop/session/c07151afb1e540a78ec7f5fb70824aaf?variant=devin
Requested by: @HuiJun

[devin-ai-integration]

I'll fix CI failures and address comments from users with write access. I'll skip comments containing "(aside)".

• Disable automatic comment, CI, and merge conflict monitoring