The README table validation work reveals that a bit more than half the specs in this repo have a TLC model associated with them. Adding TLC models to the remainder (if viable) would be an easy way to have improved confidence that the specs in this repo are actually correct (in the sense of capable of being validated, not exhibiting simple type errors, etc.) and would expand the functional test suite for the TLA+ tools.
The README table validation work reveals that a bit more than half the specs in this repo have a TLC model associated with them. Adding TLC models to the remainder (if viable) would be an easy way to have improved confidence that the specs in this repo are actually correct (in the sense of capable of being validated, not exhibiting simple type errors, etc.) and would expand the functional test suite for the TLA+ tools.