Complex sentence: Later that same year, Yuan Yu wrote the TLC model checker for TLA + specifications which was used to find errors in the cache coherence protocol for a Compaq multiprocessor.
Split into simpler sentences: Later that same year, Yuan Yu wrote the TLC model checker for TLA + specifications. TLC was used to find errors in the cache coherence protocol for a Compaq multiprocessor.