SpecForge

AI-Powered Formal Specifications

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

downloadDownload menu_bookDocs
SpecForge style=

Download

By downloading and using SpecForge, you agree to the license terms for Community/Essential, or Enterprise.
Windows
macOS
Linux
VSCode
Python SDK

Old releases and other resources are available from the releases page.

Edition

Community
For Researchers/Educators
menu_book How to Switch
cancel Commercial Use Not Allowed
check_circle No Feature Limitations
check_circle User Registration Not Required
check_circle Free

Essential

For Enterprise
menu_book How to Switch
check_circle Commercial Use Allowed
cancel Feature Limitations*
check_circle User Registration Not Required
check_circle Free
* 20 specs per project
* 3 systems per project

Enterprise

For Enterprise
check_circle License Required
check_circle Commercial Use Allowed
check_circle No Feature Limitations
check_circle User Registration Required
mail Contact Us

Clear Specs, Confident Systems

Challenges

While the evolution of AI is making systems more sophisticated, their increasing complexity and black-box nature are creating new challenges related to the development of specifications.

warning Ambiguous Requirement Specification: Frequent misinterpretations and misunderstandings lead to rework and inefficient development processes.
warning Deterioration of Quality and Productivity: Flaws in specifications directly lead to a decline in system quality and development productivity.
warning Lack of Reliability and Explainability: It is often difficult to logically investigate causes or explain operations when problems occur.

Formal Approach

'Formalization' is an approach to strictly and accurately describe system requirement specifications using mathematical notation (formal specification description languages).

thumb_up Mathematically rigorous specifications eliminate ambiguity and contradictions, preventing misunderstandings among development teams.
thumb_up Formal and logic-based technologies automate many quality assurance tasks, simultaneously improving both productivity and reliability.
thumb_up The logical representation of specifications allows for constant data monitoring and explanation of system behavior.
SpecForge

Building Trust, Formally

SpecForge supports the process of starting with informal design intent and, through iterations of formalization and analysis, 'forging' it into unambiguous and refined formal specifications.

Extraction of Design Intent

Clarify informal requirement specifications and design intent expressed in natural language, diagrams, etc.

messageLLM-powered features to generate formal specifications from natural language descriptions.
Extraction of Design Intent

Formal Specification

Describe the design intent as a formal specification based on STL (Signal Temporal Logic) using our DSL.

messageSTL is well-suited for specifying systems that deal with continuous time and analog signals.
Formal Specification

Formal Analysis and Verification

Analyze and verify consistency with data and other specifications to confirm that it aligns with the original intent.

messageWe provide state-of-the-art formal analysis and verification capabilities.
Formal Analysis and Verification

Refinement and Improvement

Modify and improve the specification based on the analysis results. Repeat this cycle to rigorously develop and strengthen the specification.

Refinement and Improvement

Use Cases for Integration

done_all

Reliable Specifications

Automatically verify if the created specifications match the intent by cross-referencing them with actual data and simulation results.

Reliable Specifications
line_axis

Test Scenario Synthesis

Generate test scenarios from specs that visualize their meaning and validate the designer's intent.

Test Scenario Synthesis
troubleshoot

Stream Data Monitoring

Continuously monitor real-time data obtained from running systems against formal specifications to detect any discrepancies or abnormalities.

Stream Data Monitoring
difference

Streamlined Delta Development

Develop specifications for new features while minimizing impact on existing ones by detecting conflicts and eliminating redundancy between specifications.

Streamlined Delta Development
insights

System Behavior Analysis

Infer and characterize the behavior of data-driven systems as explainable formal specifications (rules) from their input and output data.

System Behavior Analysis
hub

Integration with Other Tools

Export created and verified formal specifications to various ALM (Application Lifecycle Management) and design tools for consistent utilization as design assets.

Integration with Other Tools

For demonstration requests, technical inquiries, or discussions about implementation,
please don't hesitate to get in touch.

Talk to us