As software grows increasingly complex, verification becomes more and more challenging. Automatic verification by model checking has been effective in many domains including computer hardware design, networking, security and telecommunications protocols, automated control systems and others. Many real-world software models, however, are too large for the available tools. The difficulty-how to verify large systems-is fundamentally a search issue: the global state space representing all possible behaviors of a complex software system is exponential in size. This state space explosion problem has yet to be solved, even after many decades of work. This paper is structured as follows. We begin with a theoretical rationale for why random search methods like LURCH can be incomplete, yet still successful. Next, we note that for a class of problems, the complete search of standard model checkers can be overkill. LURCH is then briefly introduced and our two case studies are presented.