Summary: Output written via IO.print before a runtime trap is silently discarded. The captured stdout buffer is only returned to the CLI after successful execution; on trap the buffer is dropped as the exception unwinds.

Reproduction

public fn main(@Unit -> @Unit)
  requires(true) ensures(true) effects(<IO>)
{
  IO.print("line 1 before crash\n");
  IO.print("line 2 before crash\n");
  IO.print("line 3 before crash\n");
  IO.print("line 4 before crash\n");
  let @Nat = 42 / 0;
  ()
}

$ vera run /tmp/buffer_test.vera
Error: Runtime contract violation: error while executing at wasm backtrace:
    0:     0x62 - <unknown>!main

Caused by:
    wasm trap: integer divide by zero

Expected: the four line N before crash lines precede the trap message. Actual: all four are lost.

Root cause

The IO.print host import in vera/codegen/api.py (host_print, ~line 450) appends the decoded UTF-8 to a Python io.StringIO named output_buf — it never writes to sys.stdout directly. The buffer is only surfaced to the CLI after the WASM call completes successfully:

# vera/codegen/api.py:2442-2475 (abridged)
try:
    raw_result = func(store, *call_args)
except _VeraExit as exit_exc:
    return ExecuteResult(stdout=output_buf.getvalue(), ...)   # exit(): OK
except Exception as exc:
    # ...
    if exc_name in ("Trap", "WasmtimeError") and last_violation:
        raise RuntimeError(last_violation[0]) from exc   # <-- buffer discarded
    raise                                                # <-- buffer discarded

On trap, the raise path unwinds without doing anything with output_buf. The CLI (vera/cli.py:605) only prints exec_result.stdout after execute() returns normally. So on any trap, every prior IO.print byte is thrown away.

This is not the wasmtime runtime buffering anything — wasmtime-py calls host_print synchronously for each IO.print at the Vera source site; the buffering is entirely in our Python shim.

Impact

• Debugging by inserting IO.print calls before a suspected crash site doesn't work — the prints never reach the terminal.
• Conway's Game of Life session lost ~30 minutes to this: the agent inserted instrumentation prints, saw no output, concluded its changes weren't being exercised, and went looking for the wrong bug.
• Combined with Runtime traps need Vera-native diagnostics, not raw wasmtime stack traces #516 (mislabelled trap messages), stdout loss makes it near-impossible to tell where in a program a trap occurred.

Proposed fix

Three shapes, pick one or stack them:

1. Flush on the trap path. In the except Exception as exc: block of execute() in vera/codegen/api.py, write output_buf.getvalue() (and stderr_buf.getvalue()) to sys.stdout/sys.stderr before re-raising — or attach them to the raised RuntimeError so vera/cli.py can print them alongside the trap message. Minimal change, localised, matches existing capture semantics.
2. Tee in the host import. Change host_print to write to output_buf and sys.stdout simultaneously (optionally only when capture=False; the test harness passes capture=True and wants the current behaviour). Live output, no buffering surprise, costs one extra write per IO.print.
3. Add IO.flush() as a new effect operation letting programs flush at explicit boundaries. Lower priority — (1) or (2) makes the common case work automatically.

(1) is the cheapest and fixes the reported symptom exactly. (2) is the most user-friendly but changes observable behaviour under vera run (output appears incrementally, not as a single block after the call returns). Probably ship (1) first, consider (2) as a follow-up.

Related

• Runtime traps need Vera-native diagnostics, not raw wasmtime stack traces #516 (trap messages mislabelled — also makes debugging crashes harder)
• Surfaced during the Game of Life agent session; documented in the docs-skill-gaps thread leading to PR SKILL.md documentation sweep + bug tracking from Game of Life agent run (#513) #518.