Split from #170. The advanced-testing-features half of that issue is active-enhancement work; the Hypothesis-integration half remains in #170 as a bookmark (deferred-decision about adopting Hypothesis as an additional input-generation backend).

Features in scope

• Input shrinking — when a test fails, find the smallest input that still triggers the failure. Z3 currently returns whatever counterexample the solver finds first; smaller failures make debugging meaningfully faster, especially for Array / ADT / nested-structure inputs where the raw counterexample can be large.
• Cross-function scenarios — test sequences of function calls (e.g. put then get) to validate stateful contracts. Single-function input generation can't catch invariants that span call boundaries; effect-handler interactions are the canonical motivating case.
• Coverage-guided generation — use WASM execution paths to guide input generation toward uncovered branches. Coverage-feedback loops the generator toward failure-prone shapes (the AFL / hypothesis-coverage-guided style, but driven by WASM trace data rather than instrumented Python coverage).

Out of scope (split out)

• Hypothesis integration — kept on Evaluate Hypothesis for vera test property-based input generation #170 as a deferred bookmark. Whether to adopt Hypothesis as the engine for non-Z3-encodable types (String / Array / ADT / nested) is the deferred decision; its trigger condition is "when vera test input generation reaches its Z3 ceiling and we need a non-SMT fallback."
• Mutation testing — already tracked as Add mutation testing with mutmut for type checker and verifier #387 (mutmut bookmark). Different harness — mutmut mutates function bodies and asks "do contracts kill the mutant?" while these features mutate inputs and ask "do contracts hold for this input?". Both are useful; both are deferred.

Follow-up from

• Contract-driven testing: vera test command #79 vera test contract-driven testing (v0.0.47)
• vera test: Float64 and compound type input generation #169 vera test Float64 and compound type input generation
• Evaluate Hypothesis for vera test property-based input generation #170 (parent) vera test: evaluate Hypothesis for property-based input generation (bookmark)
• Add mutation testing with mutmut for type checker and verifier #387 Add mutation testing with mutmut (bookmark)