SpecForge – A Platform for Authoring Formal Specifications | Hacker News Reader

SpecForge – A Platform for Authoring Formal Specifications

docs.imiron.io

81 pointsagnishom12 comments

The word "AI-Powered" is shown on the front-page of this project as such:

An AI-powered platform for developers to "forge" rigorous and precise system specifications through an iterative process of formalization and analysis.

https://imiron.io/specforge/

This title should maybe include that so people are aware that if you adopt this tool, there is some expectation that AI is involved, unless it's an AI optional product, then they need to clarify.

From what I gather this marries a self-correcting formal specification based on Signal Temporal Logic (cf. https://en.wikipedia.org/wiki/Temporal_logic) with a natural language requirement definition (like OpenSpec).

STL is a spec for continuous, real-time signals over dense time that is appropriate for physical devices and real-time streams. See the "Use Cases for Integration" section in their landing page: https://imiron.io/specforge/

If I were them I would lead with how they differ from existing spec languages.

I have been thinking about how to write specifications for an AI agent to write code for a new project with detailed requirements. I was simply going write it as a list of requirements, starting at REQ001, one beneath the other, with subsequent requirements also building upon prior ones. The developed code would be intended to mark as a comment where in the code each individual requirement is implemented. There might also exist one primary unit test for each requirement. If tests are to not be implemented, then a human is more closely responsible for reviewing changes to the implementation. Over time, I would update/insert/delete individual requirements, and gaps may come to exist in their numbering, but this is okay. The numbers are sorted identifiers only, so a new requirement can even be added as say REQ033B. Overall, this is not a formal system, and it's loose enough that any human and any AI can work with it. For a formal system, an AI may even translate my prose into a formal definition language that it is familiar with, of which there are many. In conclusion, I don't think it's the job of a human to write specifications in a formal spec language.

Tend to adopt RFC standards for specs, works pretty well. My general rule of thumb is describe scope/concerns/interfaces at a high level, details at any wanted depth. That makes the LLM generated code reasonably stable and bounds it to a clearly defined boundary. Whatever ambiguity is left in details is then treated "expectedly unstable".

Do you have an example of such a spec that you can publicly share, perhaps on GitHub?

Whose formalities? The horse still comes first.

This method is certainly good to learn, but I had some difficulties understanding it

SCRUM is that my PRD you?

At least it too is Japanese.

Strong SVA vibes. Also it seems to be only free for non-commercial use. Interesting anyway!

What's that, SystemVerilog Assertion?

Nice, very LTL

Reply on news.ycombinator.com