Intent: Impl-vs-spec verification

Goal

Implement implementation-vs-spec verification for Intent — the biggest remaining correctness gap.

Current state

The compiler currently checks:

• Type correctness (HM inference)
• Spec satisfiability (Z3: are constraints self-consistent?)

It does NOT check: does the implementation satisfy the spec for all inputs?

Approach (ROADMAP.md recommended order)

Start with counterexample search (fastest to ship, highest signal): 1. For each definition with a spec, generate a Z3 query: "does there exist an input where the implementation violates the spec?" 2. If Z3 finds a counterexample, report it as a verification error with the concrete input 3. If Z3 proves unsat, report as "verified"

Then, only if counterexample search proves insufficient, move to symbolic execution (encoding pattern matching, recursion, list ops into SMT-LIB — this is harder and may not be worth it for all constructs).

Concrete deliverables

1. A new verification pass in the compiler (Verify.hs or extension of Check.hs) that takes a definition + its spec and emits a Z3 query to check impl-satisfies-spec 2. At minimum, this should work for simple arithmetic/comparison functions with scalar inputs 3. CLI: (or hook into existing ) 4. Tests covering: (a) passing case (impl matches spec), (b) counterexample found (impl violates spec), (c) undecidable/timeout fallback 5. ROADMAP.md updated to reflect status

Reference

• Existing Z3 integration: Omni/Intent/Verify.hs, Omni/Intent/Check.hs
• Spec satisfiability already uses Z3 fixedpoint — extend this path
• ROADMAP.md: Implementation-vs-Spec Verification section
• Soft exit criteria: 'at least one non-trivial fragment gets automated counterexample detection/proof support'

Notes

• Do not rewrite the type checker or synthesis loop
• Start narrow: make it work for a simple example end-to-end before generalizing
• Add to test-examples.sh or a new test-verify.sh