An experimental integration of the TLA+ runtime with the OBP2 debug and model-checking infrastructure.