The reason is obvious - LLMs got good at writing them, initial cost to write went down 99%, toil to keep them up to date with code went down 99% and some people noticed. Value proposition went from ‘you must be joking unless we’re AWS and you’re proposing an IAM code change’ to ‘plan mode may also emit TLA+ spec as an intermediate implementation artifact’.

It's not strange at all.

The second story, and highly upvoted, on HN right now is: "AI will make formal verification go mainstream"[1].

[1] https://news.ycombinator.com/item?id=46294574