Diagnostics reference¶
What the compiler tells you, and what it means.
Every entry below states the finding — what the compiler established — rather than only what failed. That distinction matters here: a zqel diagnostic is usually the result of a proof, so "invariant can be violated after one cycle" is not a guess about your code, it is a counterexample the solver constructed.
All messages on this page are real output, produced with
zqel --target check on a minimal example.
Reading a verdict¶
verification failed:
[invariant-step] invariant can be violated after one cycle: NOT y
counterexample: a=1, y=0
Three parts: the code in brackets, the claim that failed, and a counterexample — the concrete state in which it fails. The counterexample is the useful part. It names every variable the solver had to fix, so you can replay the situation by hand.
Most verdicts also carry a location, between the code and the claim:
[invariant-init] line 11: invariant does not hold in the power-up state ...
[parse-error] line 11:19: expected expression ...
It is there when the compiler knows it — a contract clause carries its line, a parse error its line and column — and absent when it genuinely does not. Some findings have no single line: a composition obligation spans two blocks, and naming one of them would be a guess. An unlocated verdict is telling you that, not withholding it.
An unknown is different from a violation, and the wording says so: a
violated property is proven wrong, an unknown means the solver could not
decide within its budget. Never read the second as the first.
Contract verdicts¶
invariant-init¶
The invariant does not hold at the power-up state — before the first scan has run, with every output and local at its default and derived definitions not yet executed.
verification failed:
[invariant-init] invariant does not hold in the power-up state, before the
first scan has run (every output and local at its default): y
counterexample: a=0, y=0
An INVARIANT claims two things: that it holds at power-up, and that it holds
after every completed scan. This diagnostic is about the first.
Usually the claim is right and the default is wrong: an output that starts
FALSE cannot satisfy an invariant demanding it be true. Either give the
register the initial value the claim needs, or weaken the claim to what holds
from the start.
There is a third possibility, and it is the common one for combinational
outputs. If the claim is a relation that only becomes true once a scan has
computed it — (live OR faults) = status, say — then it is not an invariant
at all: before the first scan the outputs it relates do not exist yet. Write
it as a RULE, which states the relation of an executed scan and carries no
power-up obligation. It is still proven; it simply is not asked a question
about a moment it says nothing about.
The exemption follows the construct, not the shape of the claim: the same
relation written as an INVARIANT keeps its power-up obligation.
invariant-step¶
The invariant holds in some state and fails in its successor. This is one-step induction: the compiler assumed your property and found a single scan that breaks it.
verification failed:
[invariant-step] invariant can be violated after one cycle: NOT y
counterexample: a=1, y=0
Read the counterexample as the state before the offending scan. Here y is
false as required, a is true, and the next scan sets y — so NOT y does
not survive.
invariant-output¶
The invariant is stated over a derived value, and it does not follow from what the registers guarantee.
A derived output is recomputed from inputs every scan, so there is no register invariant for the induction to stand on. Either state the property over the registers that carry the state, or make the value a register itself.
Both the invariant and the register premises are read at the scan boundary: the output as it is driven at the end of the scan, and the registers as they are then. A claim that mixes an output with a register therefore speaks about one state, which is what it looks like it does.
Mirroring into a register is a workaround, not the rule
Earlier revisions of this page recommended mirroring the condition into a register and stating the claim over that register. That advice existed to route around a defect — until 2026-09-03 a derived value read its registers at their next-state formula while a register named directly in the same invariant was read at the current one, so
AMP := N <= 400; INVARIANT AMP OR (N > 400);
was refused although it is a tautology. The giveaway was that freezing the register made the identical claim provable.
Mirroring is still a legitimate modelling choice when you genuinely want the condition to be state. It is not required to make an output claim provable, and it is not free: it adds a register and can add a scan of latency.
nonvacuity-unknown¶
Not a violation. The compiler checks that a property is not vacuously true — that the situation it talks about can actually arise — and the solver could not decide that within its budget.
The property may well hold. What is missing is the assurance that it says something.
Wiring and structure¶
combinational-cycle¶
A derived value depends on its own result within the same scan.
verification failed:
[combinational-cycle] combinational cycle through 'x': x -> y -> x
(a derived value depends on its own this-cycle result)
The path in the message is the whole cycle, in order — start reading at the name and follow the arrows back to it.
If the self-reference was meant to reach the previous scan, use PRE. If
it was meant as a simultaneous equation, that is a separate feature with its
own admission rule (docs/adr-algebraic-cycles.md).
missing-otherwise (warning)¶
An output has guarded rules but no OTHERWISE, so when no guard fires it
silently keeps its previous value.
warning: [missing-otherwise] output 'y': no OTHERWISE rule; when no guard
fires the output silently holds its previous value (implicit HOLD).
A warning rather than an error, because holding is sometimes exactly right.
It is worth an explicit OTHERWISE anyway: the next reader cannot tell a
deliberate hold from a forgotten case.
Rule-governed inputs¶
A sub-instance input can be given a value by a wire or by clauses, never by both (RMC-1). The three codes below are what that costs when it goes wrong.
rmc1-sink-unconstrained¶
verification failed:
[rmc1-sink-unconstrained] the governed input latch.S is missing a sufficient
clause (… IMPLIES latch.S) — without both directions its value is not
determined (RMC-1.1)
A governed input must be determined — one value for every input
assignment — not merely constrained. A permission (latch.S ONLY_WHEN Start)
never requires the input to be set; a trigger (Start IMPLIES latch.S) never
forbids it otherwise. Both directions, or the value has no single meaning and
the compiler will not choose one for you.
rmc1-sink-conflict¶
verification failed:
[rmc1-sink-conflict] the input latch.S is both wired and governed by clauses
(line 15); a sink is exactly one of the two (RMC-1.2)
Two mechanisms describing one input is one description too many. If they ever disagreed, nothing in the language would say which wins — so the question is not allowed to arise.
rmc1-unknown-instance¶
verification failed:
[rmc1-unknown-instance] 'nosuch' is not a declared instance
The clause names an instance the block does not declare. Usually a typo in the instance name; the port name is checked separately.
Signal polarity¶
INVERTED (§4.7) records that a port is active-low once, at the declaration,
so everything below it speaks about the plant rather than the wire. It is
accepted only where that statement means something.
pol1-bool-only¶
verification failed:
[pol1-bool-only] line 3:13: INVERTED is a BOOL port modifier (got INT)
Polarity is a statement about a two-valued signal. An INT has no inverse in
that sense.
pol1-ports-only¶
verification failed:
[pol1-ports-only] line 9:14: INVERTED describes the polarity of a PORT; a
local has no external side
The modifier describes the relationship between a terminal and the value the program reads. A local has no terminal, so there is nothing for it to describe.
pol1-scalar-only¶
verification failed:
[pol1-scalar-only] line 3:29: INVERTED applies to a scalar BOOL port (arrays
are deferred)
Per-element polarity on an array is deferred, not forbidden in principle — an array whose elements differ in polarity has no single answer, and the surface for saying which is which does not exist yet.
Solver-level outcomes¶
native-solver-abandoned¶
A native solver call was abandoned and this process is no longer safe for further proof work. It is never a statement about your program — restart the process and run again.
The supervised CI harness turns this into a typed SOLVER_CRASH with exactly
one retry, so a single occurrence does not fail a gate.
Typed relational clauses¶
RULE a ONLY_WHEN b, IMPLIES, IFF and EXCLUDES (§8.6a of the Language
Reference) are checked before anything can search for an implementation. The
codes below come from that pass, and they share one property worth knowing in
advance: when one of them fires, nothing was materialised. The compiler did
not adopt a partial definition and then reject it — it adopted none.
ns1-literal-not-output¶
verification failed:
[ns1-literal-not-output] the literal side of a typed clause must name a
declared BOOL output; 'helper' is not one (NS-1.2/NS-1.3)
The literal side is what the clause governs, so it has to be something the
block defines: a declared BOOL output. A misspelling lands here, and so does
an attempt to constrain an input or a local.
ns1-condition-references-output¶
verification failed:
[ns1-condition-references-output] the condition of a typed clause must not
reference its own base output 'run' (NS-1.2)
RULE run ONLY_WHEN (key AND run) says nothing: the condition under which
run may hold is allowed to mention run, so it rules nothing out and any
implementation satisfies it. Write the condition over inputs and other signals.
ns1-temporal-rung1¶
verification failed:
[ns1-temporal-rung1] a temporal clause governs output 'run', which has no
implementation: rung-1 synthesis is combinational and cannot honor signal
history. Provide an implementation for this output; the clause then becomes
an ordinary proof obligation (NS-1.9)
RULE run ONLY_WHEN HELD(key, T#100ms) asks for an output that depends on how
long something has been true, and the synthesiser that would have to invent
run sees one scan. This is a refusal rather than a silent weakening: give
run an implementation, and the same clause becomes an ordinary obligation
discharged against it.
ns1-iff-conflict and ns1-iff-unknown¶
verification failed:
[ns1-iff-conflict] the definition RULE y IFF ... collides with the remaining
clause set for some input assignment; nothing was materialised
(fail-closed, NS-1.8)
verification failed:
[ns1-iff-unknown] cannot establish that RULE y IFF ... is consistent with the
remaining clauses (a clause leaves the decidable fragment); nothing was
materialised (fail-closed, NS-1.8)
IFF defines its output, so before that definition is adopted it is checked
against everything else the block says. conflict means some input assignment
makes them contradict. unknown means the check could not be run at all — a
clause outside the decidable fragment, or a solver that did not decide.
They are different verdicts and the wording keeps them apart, but the half that matters is the same in both: nothing was materialised. An unchecked definition is not adopted provisionally.
ns1-pair-conflict (warning)¶
warning: [ns1-pair-conflict] clauses at lines 10 and 11 drive 'Release' to
both values: their antecedents demand and fault can hold at the same time
verification failed:
[synthesis-contract-unrealizable] no output satisfies all RULEs for the input
assignment [demand=True, fault=True]; colliding clauses: RULE #1, RULE #2
An explanation, not a verdict — note that it is a warning and that the failure beneath it carries a different code. The verdict comes from the ordinary proof over the whole clause set, which fails with or without it. What the pair analysis adds is which two clauses collide and why.
A necessary clause colliding with a sufficient one reads differently, because a different thing fails:
warning: [ns1-pair-conflict] sufficient clause (line 10) and necessary clause
(line 11) on 'Release' collide: the antecedent pressed can hold while the
necessary condition (NOT locked) fails
It is deliberately incomplete: a contradiction needing three or more clauses escapes it, and the verdict fires anyway. A missing warning is not a promise that the clauses agree.
Reserved, but not enforced¶
Two clauses parse and are then refused. That combination is deliberate: they were accepted once and checked by nothing, so removing them from the grammar would turn old sources into confusing syntax errors, while keeping them silently would go on looking like a promise the compiler had kept.
extern-require-undecided¶
verification failed:
[extern-require-undecided] REQUIRE of EXTERN 'fast_scale' at its call site
(line 12) is undecided: the solver returned unknown. Undecided is not
discharged.
An EXTERN's REQUIRE is an obligation on the caller and is proved at every
call site from the block's own premises (§12.1). When that proof cannot be
carried out — the clause does not encode, or the solver returns unknown —
the call is refused. A precondition that could not be checked is not a
precondition that held.
An unestablished one reports as function-require-violated, the same code an
ordinary FUNCTION uses, because it is the same failure.
extern-require-callsite-unsupported¶
The call sits in a position this slice does not cover, so the premises the obligation would be proved from do not apply to it. Refused rather than passed over.
state-error-unsupported¶
verification failed:
[state-error-unsupported] Pol2: STATE_ERROR 'y' cannot be honoured in this
language version — there is no proved state envelope for it to bound. ...
The error envelopes the compiler proves cover outputs. A bound on a state
needs its own reference point, instant, and accumulation rule, and those are
not defined, so there is nothing for STATE_ERROR to be compared against.
Acceptance policy¶
An ASSURANCE bound says how far a machine result may sit from its exact-real
meaning (§8.8). It is either discharged against a proved envelope or refused —
never carried unchecked, because from outside those two look identical.
assurance-policy-unprovable¶
verification failed:
[assurance-policy-unprovable] Pol: OUTPUT_ERROR 'nosuch' states a bound, but
this compilation has no PROVED error envelope for 'nosuch', so there is
nothing to compare it against. ...
Either the name is not an output with a proved envelope, or — the usual case —
the compilation has no numeric representation at all. Under the DEFAULT
profile MATHREAL is exact ℝ and carries no error to bound. Compile with
--profile float64, or a project configuration that sets a representation.
assurance-policy-not-constant¶
verification failed:
[assurance-policy-not-constant] Pol: the bound on OUTPUT_ERROR 'y' is not a
numeric literal. ...
The threshold is compared against a proved envelope at compile time, so it has
to be a constant the compiler can read. 1.0e-15 + 1.0e-15 is refused rather
than skipped.
RequirementViolation (not a finding code)¶
The fourth outcome is not a [code] at all — it is an exception carrying
output 'y' is PROVED to |err| <= 3.064e-15, but the ASSURANCE policy demands
<= 1.000e-30; the proof succeeded, the acceptance policy failed
Read the wording carefully, because it says something the three codes above do not: the proof went through. What failed is the bound you asked for, not the mathematics. Either the policy is too tight for the arithmetic, or the arithmetic needs restructuring to earn it.
Adding to this page¶
If you meet a code that is not here, that is a documentation gap and worth reporting. The list is deliberately not exhaustive: it covers the diagnostics an engineer meets while modelling, not every internal code the compiler can emit.