I will give an outline of the Must project, a framework for modeling and state space exploration of 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, as well as our attempts to bridge the gap between model and code and between (randomized) state space exploration for fixed configurations and guarantees for unbounded systems. I will also describe the challenges of deploying modeling and model checking in an industrial context.