How does this compare to previous generations of specification-driven development using formal methods?

I think semcheck has a different use-case. AI is inherently imprecise, if you need formal mathematical verification, AI isn't suitable for that. What semcheck does give you is a very simple way to start verifying specifications, and it's best used in combination with AI-assisted development workflows where you're already spending a lot of time writing specifications (i.e. prompts).