Hi! First, thank you for the useful verifier diagnostics here. I may be misunderstanding the intended relationship between vera test and vera verify, but I found a small case where vera test --json reports success/verified for a program that vera verify --json rejects and vera run fails on at runtime.

Version: vera 0.0.155, repo HEAD 08c1197d4d701fc429cc448abb89a8d08b2f7b7c.

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)
}

Observed behavior

vera check --json wrong_double_initial.vera succeeds:

{"ok": true, "diagnostics": [], "warnings": []}

vera verify --json wrong_double_initial.vera exits 1:

{
  "ok": false,
  "diagnostics": [
    {"error_code": "E500", "description": "Postcondition does not hold in function 'double'."}
  ],
  "verification": {"tier1_verified": 3, "tier3_runtime": 0, "total": 3}
}

This looks expected: the body returns x + x + 1, while the postcondition claims x + x.

vera run wrong_double_initial.vera exits 1:

Error: Postcondition violation in double(@Int -> @Int)
  ensures(@Int.result == @Int.0 + @Int.0) failed

vera test --json wrong_double_initial.vera exits 0:

{
  "ok": true,
  "functions": [
    {"name": "double", "category": "verified", "reason": "Tier 1 (proved)", "trials_run": 0},
    {"name": "main", "category": "verified", "reason": "Tier 1 (proved)", "trials_run": 0}
  ],
  "summary": {"verified": 2, "tested": 0, "total_trials": 0, "total_failures": 0}
}

Expected behavior

I would expect vera test --json not to return a green ok: true / verified result for a program whose contract verification fails with vera verify --json.

Possible ways to avoid the false-green signal:

• test --json invokes/reuses the same verification gate and returns nonzero with the E500 diagnostic; or
• test --json reports these functions as unverified/failed/skipped rather than category: "verified"; or
• if test intentionally has narrower semantics than verify, the JSON output makes that boundary explicit so downstream automation does not treat this as proof success.

Why this matters

JSON status is likely to be consumed mechanically by CI pipelines and downstream tooling. A false-green ok: true from test --json, especially with category: "verified" and reason: "Tier 1 (proved)", can cause a build step to accept a contract-incorrect program even though verify --json correctly rejects it.

Question

I am treating vera verify --json as the authoritative contract/proof gate. If vera test is intentionally meant to skip or only partially reuse verification in this situation, the bug may be in my expectation or in the JSON wording (verified / Tier 1 (proved)) rather than in the underlying test behavior.

Would you expect vera test --json to be a safe green gate for contract correctness, or should downstream tools always run vera verify --json separately and treat test --json as corroborating/runtime evidence only?