SpecForge – A Platform for Authoring Formal Specifications

(docs.imiron.io)

79 points | by agnishom 2 days ago ago

13 comments

  • giancarlostoro a day ago ago

    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.

  • 15 hours ago ago
    [deleted]
  • itomato a day ago ago

    Whose formalities? The horse still comes first.

  • abbasov_murad 2 days ago ago

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

  • effnorwood a day ago ago

    SCRUM is that my PRD you?

    • OutOfHere a day ago ago

      At least it too is Japanese.

  • esafak a day ago ago

    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.

  • poslathian a day ago ago

    Nice, very LTL

  • OutOfHere a day ago ago

    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.

    • mrbnprck 10 hours ago ago

      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".

      • OutOfHere 3 hours ago ago

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

  • IshKebab 2 days ago ago

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

    • esafak a day ago ago

      What's that, SystemVerilog Assertion?