Summary

Runtime traps from the WASM runtime bubble up as raw wasmtime stack traces with hex offsets, not as Vera diagnostics. Compile-time errors have carefully crafted "Fix:" suggestions; runtime traps don't. An agent hitting a GC bug / integer overflow / bounds check trap has no actionable information.

Example

From the Game of Life agent run that surfaced #515:

Error: Runtime contract violation: error while executing at wasm backtrace:
    0:    0x33e - gc_collect
    1:    0x1b9 - alloc
    2:    0x55f - cell_at
    ...

Caused by:
    0: memory fault at wasm address 0x180000 in linear memory of size 0x180000
    1: wasm trap: out of bounds memory access

Three problems in this one output:

1. "Runtime contract violation" is often wrong: vera/cli.py:654 blanket-labels every Trap/WasmtimeError as a contract violation:

   if exc_name in ("Trap", "WasmtimeError"):
       msg = f"Runtime contract violation: {exc}"

   But traps include out-of-bounds memory access (GC bug or array OOB), integer overflow (INT64 saturation), unreachable (compiler asserts), and stack overflow — none of which are contract violations. Agents and humans reading the first line dismiss real compiler bugs as "my contract is wrong."

2. Stack offsets are hex WASM addresses: 0x33e tells nobody anything. Even with symbol names (gc_collect, alloc), there's no source-line mapping — runtime traps from user functions like cell_at don't tell the user which line of cell_at faulted.

3. No actionable guidance: Compile-time errors are a paragraph — what went wrong, rationale, fix, spec reference. Runtime traps are a stack trace. Contrast E130:

   Unresolved slot reference. @Int.3 has no matching binding.
   Fix: ...
   

   with the trap above. The former helps; the latter requires WASM internals to interpret.

Proposed scope

Staged improvements, each an independent PR:

Stage 1: Categorise the trap reason (small, high impact)

Parse the wasm trap: ... tail of the error and map to distinct human categories:

The existing "Runtime contract violation" should be reserved for $contract_fail (the actual contract-failure trap, which has a distinct WASM-abort path that could be recognised by the function-import tag).

Stage 2: Source-map the Vera function that trapped

The stack trace has <unknown>!cell_at — we know the function name; can we go one better and point at the line of cell_at where the trap happened? The WASM offset within the function is in the stack frame (0x55f); if we emit a side-table mapping offset ranges to source lines at compile time, we can translate it.

Low priority — a full DWARF-style debug-info path — but even a coarse "trap inside cell_at at or after line 84" would be a big step up.

Stage 3: Specialised help for common trap classes

For the out of bounds memory access class: show the allocator stack (which we already have in the backtrace) and suggest profiling options (what's a recent allocation size, what's the current heap pressure). Most of the time these traps are the user triggering a known bug (#487, #515) and the diagnostic should point there explicitly.

Motivation

The agent self-observation that motivated this issue:

The entire reason this program took as many rounds as it did isn't that the language is hard — once you internalise the De Bruijn discipline, the slot arithmetic becomes pretty mechanical — but that type-checking passed on the first version while runtime WASM execution didn't. That's a meaningful thing to know about Vera's current state: the gap between "the type system is happy" and "the compiled artefact actually runs" is wider than you'd expect from a language with SMT-verified contracts.

The language's competitive advantage is contract-verified code that LLMs can write. Runtime traps with opaque messages undermine that advantage — the verifier said yes, the compiler said yes, then the program crashed and the tooling offers nothing. Closing this gap is the highest-leverage agent-adoption improvement available.

Not in scope

• Fixing the underlying trap-producing bugs (those are separate issues: GC $alloc grows memory by only 1 page — large single allocations trap #487, Closures capturing heap-allocated values produce invalid WASM (nested-closure case is a narrow instance) #514, GC collect itself faults with out-of-bounds memory access under sustained allocation pressure #515).
• Source maps at full fidelity — Stage 2 is coarse-grained only.