Abstract Formal methods enable the verification of system behavior against requirements that are expressed as formal, mathematical properties. However, translating the often ambiguous natural language requirements that are typically produced by developers and engineers into precise mathematical specifications remains a significant bottleneck in the formal verification process. NASA’s Formal Requirements Elicitation Tool ( FRET ) is an open source tool that addresses this challenge by bridging the gap between natural language requirements and formal specifications that are suitable for automated verification. FRET enables practitioners to express requirements in FRETish , a structured natural language, that balances intuitive readability with formal rigor. FRET automatically translates these requirements into formal properties that verification tools can directly process. This tutorial paper introduces FRET and guides readers through expressing requirements in FRETish . We present the tool’s key analysis capabilities, including simulation, realizability checking, test-case generation, and automated generation of verification conditions for external formal verification tools. Our goal is to provide a comprehensive guide that helps practitioners, regardless of their formal methods background, to effectively leverage FRET in their verification and validation (V&V) workflows.