This talk presents work on comparing traces obtained from executions of distributed programs against formal specifications, written in the TLA+ formalism, of the algorithms the programs are expected to implement. We reduce the problem to a constrained model checking problem, realized using the TLC model checker. We implemented a framework that helps instrumenting Java programs for recording traces and that contains a collection of TLA+ operators used for checking traces against the specification. Traces may record updates to some of the variables used in the specification, as well as on actions the program transitions correspond to. We have applied the technique to several distributed programs, detecting discrepancies between the specifications and the implementations in all cases.