If you use LLMs to digest and summarise software maybe it can help to improve formalisation. In contrast if you use LLMs to produce more code this is contra-dictionary. More codes increases the bug surface circa logarithmically and correspondingly makes formalisation much harder as well. I want to see LLMs be used to strip away code. Only then will I believe they’re really actually good at what they’re doing.