A conventional test checks a path someone thought of. Property testing checks a statement that has to hold across paths nobody wrote down. The statement is the oracle, and the explorer's job is to find the input that breaks it.
That makes the explorer a search problem, not a test problem. Most of the result comes from which action it tries next.
Properties, not cases
A property is a sentence that must always be true. For a mobile app, one useful property is simple: the app stays alive. Not "the Reminders screen renders" and not "tapping Done saves an item" — just: whatever happens, the process should not die.
A property like that is cheap to state and expensive to check exhaustively. The explorer takes actions, observes state, and looks for a transition that violates the property. When it finds one, it has a counterexample: a sequence of actions that kills the app.
The Reminders example
We pointed an explorer at an iOS app and stated the property as the app staying alive. It violated the property in a way the happy path never would: it left Reminders, wandered into Settings, and the app died. That is a lifecycle bug, and it lives in the interaction between two screens rather than in either screen's tests.
To run on iOS we forked bombadil, a property-based testing tool for web and terminal UIs, and added an iOS driver. The driver gives the explorer a set of actions and a way to observe state. The property stays the same.
Choosing the next action
An explorer that picks actions at random spends most of its budget on transitions that lead nowhere. A smarter selection policy reads the current state and proposes the action most likely to reveal something.
This is where a model fits naturally. The state is structured, the action set is finite, and the objective is immediate: find a violation, or reach an unexplored region. In one run, jev — the state explorer we have been building — picked the right action about 3x more often than random and ended up exploring 5x more states.
The absolute numbers matter less than the shape. Better action selection multiplies the value of every step the explorer takes. The same property, the same driver and the same machine produced more coverage because the search was better.
Why this matters for agents
Agents are good at producing actions. They are less good at deciding which action is worth taking, and that is the scarce skill in verification. A model that can look at a state and choose the next check is doing the same job as a test selector: spend the next unit of work where it can change the answer.
The connection to CI is direct. A pipeline that runs everything is a random walk through the test suite. A pipeline that chooses the tests the change can reach is a guided search. Both are trying to answer the same question — is this change correct? — and both get more useful when the choice of what to run next improves.
What this does not prove
One property on one app is not a benchmark. A model-guided explorer can be wrong, and a wrong action costs a step just like a random one. The property is only as strong as its statement; "the app stays alive" catches crashes and misses incorrect behavior.
The driver is a fork, and the integration is new. The result is an argument for the approach, not a claim about how far it scales.
What it does show is the direction. If action selection improves, exploration gets cheaper at the same time, and the same amount of compute finds more. The interesting question is how much of verification turns into this shape: a property, an action set and a policy for choosing what to try next.