req language#

req is a requirements-as-code language: specifications can be written in plain natural language and formal mathematical expressions. This is progressive formalization: start with English, formalize only where it is beneficial.

Start with the Getting Started guide.

What is req?#

On most projects, a requirement lives in three disconnected places: a sentence in a document or ALM tool, a box in an architecture model, and a check buried in verification code. Keeping these three in sync is manual, and they drift apart the moment the project moves — a renamed component, a changed threshold, a link nobody updated. This is the authoring gap, and it is a major reason model-based and formal verification practices — despite being technically mature — struggle to pay for themselves in day-to-day engineering.

req closes that gap by making the requirement the single artifact. The glossary, the formal expressions, and the traceability links all live inside the requirements you already write, instead of in separate tools you have to keep synchronized by hand.

  • Requirements-centric — the requirement is the unit you author, review, and trace; there is no separate model or diagram competing for that role.

  • Model-as-glossary — the terms your requirements reference are your model: a structured glossary, not a parallel diagram to keep in sync.

  • Minimal constructs — packages, parts, attributes, requirements. Nothing else to learn before you are productive.

  • Formalism plurality — plain-text, boolean logic, set theory, algebra, temporal properties: use whichever formalism actually fits the requirement.

  • Modularity and standardization — parametric templates, similar to generics in programming languages, let requirement patterns and glossary terms be reused across teams and projects instead of rewritten each time.

  • Formal traceability — a refinement link is checked against the glossary terms it uses, not merely verified to point somewhere.

Progressive formalization — informal and formal requirements in the same file#
 package System
   part Wheel
     let deceleration_duration in real [s]
     let is_decelerating in boolean
     let speed in real [m/s]
   part

   @@
     # Rationale

     As per client email
   @@
   requirement Wheel_deceleration is
     @@
       The [[Wheel]] shall decelerate within 3s.
     @@
   requirement

   # verification simulation #
   requirement Wheel_deceleration_duration
     refines Wheel_deceleration is
     deceleration_duration = 3
   requirement

   # category sil4 #
   # verification model-checking #
   requirement Stopped_after_deceleration
     refines Wheel_deceleration is
     is_decelerating implies eventually speed = 0
   requirement
 package

Features#

req embeds markdown for rich-text formatting, images, tables and graphs — the same authoring surface as any document, without the drift. Every requirement, formal or not, can be statically analyzed against requirements-engineering best practices as you write it. When deeper structural analysis is needed, the glossary can be exported to a modeling language rather than req trying to reinvent one.

Formal requirements are recognized by their shape: a temporal property signals model checking, a real-valued equation signals simulation, a propositional expression signals constraint solving. req is designed as a front-end that routes each formal property to the adequate verification back-end — model checking, simulation, and constraint solving are on the roadmap, not shipped today.

Built for agents, too. With the rise of LLM-aided, spec-driven development, a structured, typed specification grounds agentic workflows and prompts far more reliably than markdown prose — req was designed for that kind of grounding as much as for human authoring.

The req eco-system comes with several tools for both editing and visualization:

Note

req is under active development. The language and this documentation are subject to change. See the Language Reference for the current stable specification.

Contents: