v0.4.0 - the verification release

The verification release. Unspaghettit moves from describing behavior to proving it.

Added

• Verified coverage - prove the code matches the spec, and gate on it (unspa coverage ingest, unspa check --min-verified).
• Bounded model checking + liveness/reachability goals - prove "good is reachable", not just "bad never happens".
• Project-level (cross-feature) invariants and cross-feature event coherence.
• Spec→code drift (get_drift) and a headless unspa check gate + unspa ci scaffold.
• Dashboard Verify view with navigable counterexample traces; reachability-goals editor.
• Global search across the whole model (⌘K / Ctrl+K).

Changed

• Wider MCP-tool test coverage and an ESLint + Prettier lint gate in CI/prepublish.

Full notes: see CHANGELOG.md.