I will give an outline of the Must project, a state space exploration tool for distributed systems written in a mainstream programming language (Rust). I will describe some recent technical advances that allow us to scale to large state spaces. I will also describe the challenges of deploying modeling and model checking in an industrial context. In short, I will argue that software model checking of large-scale implementations remains very much an open problem.