What's Changed
Highlights
Clearer VC error messages (#464) — Refinement failure diagnostics now split failing supertype conjunctions into separate sub-obligations, drop inert preconditions that do not affect the goal, and use a unified display pipeline for CLI/LSP error output.
Full diff: v4.3.0...v4.3.1