Skip to content

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 LoLa 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 lola --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

rmc1-sink-conflict

An instance input is both wired and governed by clauses. A sink is exactly one of the two: remove the wire, or remove the clauses.

rmc1-sink-unconstrained

The clauses over a governed input leave its value open. A trigger (X IMPLIES inst.P) and a permission (inst.P ONLY_WHEN X) are both needed; either alone determines nothing.

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.

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.