There are now projects like Specula that, using LLMs, enable us to derive specifications from the implementation, and somewhat paradoxically, use those specific

There are now projects like Specula that, using LLMs, enable us to derive specifications from the implementation, and somewhat paradoxically, use those specifications to find bugs in the implementation. https://muratbuffalo.blogspot.com/2026/08/specula-scaling-formal-specifications.html https://muratbuffalo.blogspot.com/2026/08/specula-scaling-fo... Secondly, I think the open partial specs, composable specs would help address the problems with monolithic specs that Dodd's cites. https://muratbuffalo.blogspot.com/2026/08/composition-and-modular-verification-of.html https://muratbuffalo.blogspot.com/2026/08/composition-and-mo...