Verifying the absence of partial deadlocks in Go programs is challenging when channel operations and capacities are determined at runtime. I describe two approaches that address this challenge. The first performs bounded model checking of concurrent behaviors, handling statically unknown parameters while scaling to large programs. The second translates Go fragments to a core language encodable in off-the-shelf solvers, automatically verifying deadlock freedom or inferring preconditions when safety is conditional. I will report on our experience applying this approach on a real-world codebase containing hundreds of challenging program fragments.