Hi! I noticed a small diagnostic-wording improvement that may make E500 postcondition failures easier to act on.

This concerns E500 diagnostic wording only. It does not propose changing verification semantics, and it does not resolve the separate vera test --json green vs vera verify --json red disagreement.

Evidence checkout:

• Vera HEAD inspected: 08c1197d4d701fc429cc448abb89a8d08b2f7b7c
• Source status at inspection: clean
• Repro command: vera verify --json wrong_double_initial.vera

Minimal repro

public fn double(@Int -> @Int)
  requires(true)
  ensures(@Int.result == @Int.0 + @Int.0)
  effects(pure)
{
  @Int.0 + @Int.0 + 1
}

public fn main(@Unit -> @Int)
  requires(true)
  ensures(@Int.result == 42)
  effects(pure)
{
  double(21)
}

The program type-checks but fails vera verify --json with E500. Runtime also fails the postcondition.

Current JSON excerpt

{
  "error_code": "E500",
  "description": "Postcondition does not hold in function 'double'.\n  Counterexample:\n      @Int.0 = 0\n      @Int.result = 0",
  "rationale": "The SMT solver found concrete input values for which the postcondition is false. This means the function body does not satisfy its ensures() contract for all valid inputs.",
  "fix": "Either strengthen the precondition (add a requires() clause that excludes the counterexample inputs) or weaken the postcondition to match the actual function behaviour.",
  "spec_ref": "Chapter 6, Section 6.4.1 \"Verification Conditions\"",
  "source_line": "  ensures(@Int.result == @Int.0 + @Int.0)"
}

Feedback

The current E500 diagnostic is already useful: it names the failing function, points at the ensures, includes a counterexample, and links to the relevant spec section.

The narrow concern is that the fix field names two repair classes:

1. strengthen the precondition;
2. weaken the postcondition.

For many E500 cases, a third repair class is also plausible: change the implementation so it satisfies the existing ensures clause. The verifier should not imply that it knows whether the implementation, precondition, or postcondition is the intended source of truth. The user-facing hint could still be more complete by listing all three classes without prioritizing one as correct.

Proposed wording

Proposed fix text:

Resolve the mismatch between the function body and its contract: fix the implementation so it satisfies this ensures() clause, strengthen requires(...) if the counterexample is outside the intended input domain, or weaken/change ensures(...) if the postcondition overstates the intended guarantee.

Shorter variant:

Resolve the counterexample by fixing the implementation, strengthening requires(...), or weakening/changing ensures(...), depending on which part does not match the intended behavior.

I prefer the first wording because it names all three repair classes while preserving the verifier's neutrality: the diagnostic reports an inconsistency, not which artifact is conceptually wrong.

Exact search / PR-feasibility evidence

Commands run from the Vera checkout at 08c1197d4d701fc429cc448abb89a8d08b2f7b7c:

grep -R -n -F --exclude='*.pyc' --exclude-dir='__pycache__' "Either strengthen the precondition" tests vera pyproject.toml README.md || true
grep -R -n -E --exclude='*.pyc' --exclude-dir='__pycache__' "E500|Postcondition does not hold|postcondition|requires\(\)|ensures\(\)|fix" tests vera | head -200 || true
grep -R -n -E --exclude='*.pyc' --exclude-dir='__pycache__' "strengthen the precondition|weaken the postcondition|actual function behaviour|fix the implementation|requires\(\.\.\.\)|ensures\(\.\.\.\)" tests vera || true

Relevant result:

vera/verifier.py:1306:                "Either strengthen the precondition (add a requires() clause "
vera/verifier.py:1308:                "postcondition to match the actual function behaviour."
tests/test_verifier.py:358:    def test_violation_has_fix_suggestion(self) -> None:
tests/test_verifier.py:369:        assert errors[0].fix != ""
tests/test_verifier.py:370:        assert "precondition" in errors[0].fix.lower() or "postcondition" in errors[0].fix.lower()

Interpretation:

• The exact full fix literal was found in vera/verifier.py; existing source tests in tests/test_verifier.py assert that the fix is non-empty and mentions precondition or postcondition, but do not pin the exact literal.
• A wording-only patch still needs a focused regression test because existing coverage does not assert that all intended repair classes are listed.

Feasibility recommendation

Recommendation: issue first or small diagnostic PR candidate, depending on maintainer preference.

Rationale:

• The likely source change is localized to the E500 fix= literal in vera/verifier.py::_report_violation.
• The change is diagnostic-only and should not change verifier semantics.
• The exact-string search above did not find source tests pinning the full current fix literal.
• A focused regression test should assert that the E500 fix names all three repair classes without treating implementation repair as the verifier's preferred answer.

Sketch of tiny patch (not applied)

diff --git a/vera/verifier.py b/vera/verifier.py
@@
-            fix=(
-                "Either strengthen the precondition (add a requires() clause "
-                "that excludes the counterexample inputs) or weaken the "
-                "postcondition to match the actual function behaviour."
-            ),
+            fix=(
+                "Resolve the mismatch between the function body and its "
+                "contract: fix the implementation so it satisfies this "
+                "ensures() clause, strengthen requires(...) if the "
+                "counterexample is outside the intended input domain, or "
+                "weaken/change ensures(...) if the postcondition overstates "
+                "the intended guarantee."
+            ),

Suggested test assertion shape (not applied):

err = next(d for d in result.diagnostics if d.error_code == "E500")
fix = err.fix.lower()
assert "implementation" in fix
assert "requires" in fix
assert "ensures" in fix or "postcondition" in fix

Scope boundaries

• This note does not recommend changing verification semantics.
• This note does not resolve the separate vera test --json / vera verify --json disagreement.
• No GitHub issue, PR, branch, commit, push, or external post was created.