As an example, your search graph might define your nodes as possible application states and the edges as actions to transition to a new state.
Some edges might be "create a post" and "change post privacy settings". You might then define an invariant saying "after a user creates a post the new post is in their follower's timeline if privacy settings allow".
Your search might eventually come across some set of actions that lead to this invariant being violated which is a discovered bug, e.g. if a user A creates a post -> user A changes settings to private -> user B can still see the post.
Since the search space is infinite, the effectiveness is heavily influenced by how much time you can spend searching the tree & how fast you can evaluate states. This is a kind of exploratory test & wouldn't replace unit/integration tests, but it does let you catch certain kinds of bugs that would be impossible to find otherwise.
