This isn't work I'm planning to do anytime soon but it would be a nice little project if someone else wants to take it on. Markdown is a very difficult language to work with, tooling-wise, but there are nice full-featured parsers like goldmark (used by the Hugo static site generator, for example) which make it tractable. A CI script could parse the README.md file with goldmark, find the table & its entries, and check its correspondence to the manifest.json file. This would include not only the existence of specs in the table but also whether they are properly labeled as including proofs, pluscal, TLC models, and whatever other traits we care to define. This could also implement whatever clustering & categorization is desired in #15. This could all possibly be implemented as a goldmark extension. Alternatively, there are a number of python markdown parsers of varying quality levels that could be used.