Guide

Frequent Questions

Short answers to questions that come up often.

Formal Verification

What is "verified"?

What exactly does the Z3 check prove?

One thing, precisely: that the formal claims extracted from your specs are mutually consistent, per spec and across all specs merged. It catches requirements that contradict each other before an agent spends an hour (and your tokens) building against them. It proves nothing about the generated code. See Spec Verification for a worked example of the spec-to-formula mapping.

Where are the gaps?

Three, and each is worth knowing by name:

• Extraction: an LLM translates prose into formulas, and it can mistranslate. Overplane mitigates this by requiring every formula to carry a rationale quoting the spec sentence it came from, so the mapping is auditable (see IR Generation).
• Coverage: claims about visual polish, parsing quality, or timing are not encodable in SMT and are explicitly skipped (marked non_smt in the IR).
• Implementation: a consistent spec can still be implemented wrongly. Closing that gap takes code-level verification, which Overplane supports through the IR (next question).

Can verification reach the generated code?

Yes, by writing specs that consume the IR. The rustdis example does this twice: spec #0006 derives a proptest suite where every property is named after the IR node it checks, and spec #0007 drives Kani , a bounded model checker for Rust, to prove panic-freedom of the store's pure core for all inputs up to a bound. Property tests sample the input space; Kani exhausts it. Details and code samples are in Codegen with IR.

So is this real formal verification?

The solver runs are real: Z3 decides satisfiability of the merged model on every build, and Kani (where a spec requests it) performs genuine bounded model checking. What is not formal is the translation into and out of the formal layer, which is done by LLMs. Treat the pipeline as a strong, cheap consistency net plus an audit trail from every requirement to a named formula and (optionally) a named test, not as an end-to-end proof of correctness.