Pairing a language model with a classical solver, an exact rule-crunching program, promises reasoning that is sound by construction, since the solver decides the hard step and returns an answer that can be checked independently. The catch is that trust does not disappear. It moves to the edges, into the act of turning a messy sentence into a precise spec and the act of reporting the result back, which is where most of the recent research now lives.