The paper introduces a novel intermediate representation OnionL, which decomposes requirements into a compositional tree composed of semantic scopes, logical relations, and atomic propositions, thereby enabling structured and verifiable translation.

We propose TlCrafter, a human-in-the-loop tool for formalizing software requirements into temporal logic. The main workflow of TlCrafter is illustrated in the following Figure, which consists of the following steps:

（1）Logic Recommendation: TlCrafter begins by analyzing the input natural language (NL) requirement to recommend a suitable target logic from {LTL, CTL, STL}. This recommender is designed to be both explainable and overrideable: it reports the specific linguistic cues supporting its decision (e.g., metric time bounds suggesting STL, or existential branching suggesting CTL). Users review these cues and may force a different logic type if desired, ensuring the subsequent formalization aligns with the intended verification domain.

（2）NL-to-OnionL+ Decomposition: Based on the selected logic, TlCrafter constructs an OnionL+ tree from the NL input. This step transforms unstructured text into a structured intermediate representation, making explicit the requirement’s operator structure (scopes, relations) and leaf predicates (atomic signal/state constraints). The decomposition is logic-aware: for STL, the tree supports interval-annotated temporal scopes and real-valued signal predicates; for CTL, it integrates explicit path-quantified temporal scopes. This structured representation serves as the foundation for both deterministic compilation and user interaction.

（3）Human-in-the-loop Refinement: To bridge the semantic gap between natural language and formal logic, TlCrafter provides a visual tree interface for inspecting and editing the OnionL+ structure. Users can refine the specification by correcting scope attachments, operators, intervals, and predicates through structured edits. Furthermore, after confirming the tree structure, the user can require TlCrafter to generate a temporally explicit NL paraphrase aligned with the validated structure. This feedback mechanism helps users resolve ambiguity and reduces the risk of “silent” semantic mismatches.

（4）Validation and Deterministic Synthesis: In the final stage, the backend validates the OnionL+ trees using a logic-dependent typing discipline. This involves checking operator arity and well-formedness, enforcing logic-specific constraints (e.g., CTL path quantification or STL intervals), and normalizing predicate leaves into a canonical schema. Once validated, the tool deterministically compiles the OnionL+ tree into a unique formal formula. This process ensures the syntactic correctness of the output and produces standardized specifications suitable for downstream verification tasks.