When no helper is in sight and k-induction will not close, the next question is whether the tool can find the invariant itself. Clause-learning engines do exactly that, and their verdicts quote frames, depths and blocked cubes. Reading those reports starts with knowing what a frame is: the set of states the engine believes reachable within a given number of steps, over-approximated, refined until one frame proves itself inductive.
Frame 0 is the set of reset states. Frame i is an over-approximation of the states reachable in at most i steps: it contains all of them and possibly more, the frames only shrink toward the truth, each frame sits inside the next, and each frame's image sits inside the next frame. The engine repeatedly takes a state of the top frame that violates the property and asks whether the previous frame can step into it. If a predecessor exists, that predecessor must be blocked first, recursively, and if the chain of predecessors reaches a reset state the violation is real and the chain is the counterexample. If no predecessor exists, the state is removed from the frames up to the top: it has been shown unreachable relative to the frame below. After the top frame is clean, a new frame is opened and propagation pushes every removed state as far up as it will go. When all removals of some frame have been pushed up, that frame equals the next one, it is closed under steps, it contains the reset states and excludes the bad states: an inductive invariant, and the property is proven.
What this adds over computing the whole backward reachable set is selectivity: the engine only blocks states that show up as obstacles, only relative to the frame below, and a real engine removes a generalised cube of states per solver call instead of one state, with a solver finding predecessors. The toy below uses explicit sets so the mechanism is visible; it removes single states and has no solver.
The script runs the loop above on the 16 counter states with enable free, reset state 0 and bad state 15. Each round it prints the frame sizes: frame 1 starts at 15 states (only 15 is blocked), then each round blocks the next predecessor in the unreachable chain, 14, 13, 12, 11 and 10, until the frames settle at 10 states, 0 to 9. The final frame is checked to contain the reset state, exclude 15 and be closed under steps. On the unsafe variant, where 9 is declared bad, the chain of predecessors reaches the reset state and the engine returns the path 0 to 9 instead of an invariant. The failing partners are an unsafe system that must not return proven and three candidate invariants, one of which is not inductive and one that contains the bad state, which the same checker rejects.
N = 16
ALL = set(range(N))
def succ(s, last=9):
return {s, 0 if s == last else (s + 1) % N}
def image(S):
return {t for s in S for t in succ(s)}
def ic3(init, bad, limit=40):
blocked = [set(), set()] # blocked[i]: states removed at frame i and below
def frame(i):
if i == 0:
return set(init)
out = set(ALL)
for j in range(i, len(blocked)):
out -= blocked[j]
return out
def block(s, i, trail):
if s in init:
return trail # a reset state cannot be blocked: real counterexample
while True:
preds = {p for p in frame(i - 1) if p != s and s in succ(p)}
if not preds:
blocked[i].add(s) # unreachable in i steps relative to frame i-1
return None
p = min(preds)
found = block(p, i - 1, [p] + trail)
if found is not None:
return found
log, k = [], 1
while k <= limit:
while frame(k) & bad: # blocking phase on the top frame
s = min(frame(k) & bad)
found = block(s, k, [s])
if found is not None:
return "counterexample", found, log
blocked.append(set()) # open a new top frame
k += 1
for i in range(1, k): # propagation: push removals up while no predecessor exists
for s in sorted(blocked[i]):
if not {p for p in frame(i) if p != s and s in succ(p)}:
blocked[i].discard(s)
blocked[i + 1].add(s)
log.append([len(frame(i)) for i in range(k + 1)])
for i in range(1, k): # frame invariants of the algorithm
assert frame(i) <= frame(i + 1) and image(frame(i)) <= frame(i + 1)
assert set(init) <= frame(i) and not (frame(i) & bad)
for i in range(1, k):
if not blocked[i]:
return "proved", frame(i), log
return "unknown", None, log
def is_inductive_invariant(F, init, bad):
return set(init) <= F and not (F & bad) and image(F) <= F
status, inv, log = ic3({0}, {15})
assert status == "proved", status
assert inv == set(range(10)), sorted(inv)
assert is_inductive_invariant(inv, {0}, {15})
assert log[0][1] == 15 and log[-1][1:] == [10] * (len(log[-1]) - 1), log # frames settle at 10 states
assert len(log) == 6, log # 15, 14, 13, 12, 11, 10 blocked in turn
ustatus, path, _ = ic3({0}, {9})
assert ustatus == "counterexample", ustatus
assert path[0] == 0 and path[-1] == 9
assert all(b in succ(a) for a, b in zip(path, path[1:])), path
# injected data: a false proof claim about the unsafe system, and candidate invariants
assert ic3({0}, {9})[0] != "proved"
assert not is_inductive_invariant(set(range(9)), {0}, {15}) # 8 steps to 9, which leaves the set
assert not is_inductive_invariant(set(range(10)) | {15}, {0}, {15}) # contains the bad state
print("PASS: frames settle at 0..9, an inductive invariant; the unsafe variant returns the path 0..9")The report names the invariant the engine found, not just the verdict.
Frames and depths in the log move monotonically: each frame sits inside the next, and a frame that regrows states is a defect signal.
The engine-found invariant is reviewed like a hand-written helper before signoff.
When a learning run stalls, read frames first: frames that keep growing without stabilising point at a wide datapath the solver cannot generalise, which abstraction or a hand-written helper cures. When it reports proven, extract the final frame and check it yourself with the closure test above: it contains the reset states, excludes the bad states, and every successor of every frame state stays inside.
Only 14 can step into 15, so it is the first predecessor that has to be blocked, and each removal exposes its own predecessor. The order is forced by the successor relation, and it mirrors how a solver reasons outward from the bad state one obstacle at a time.