Galois Loop Lab

Explore Bidirectional Obligation Carving on small boolean relations.
Click counterexamples, watch closures compute, compare with plain CEGIS.

Spec(x, y) relation

Current state

Ct (surviving candidates):
Ut (uncovered obligations):
Ψ(Ct) (discharged):
Dt ⊆ Ψ(Ct)  ✔
Loop complete! All obligations discharged or candidate found.

Progress metrics

|Ct|
|Ut|
|C| + |U|

Actions

Event log