# Coherency through formalisations of Structured Natural Language, A case study on FRETish

arXiv: https://arxiv.org/abs/2605.10462 · HTML: https://mlsanity.com/paper/2605.10462/

## Key facts

- No citing papers in the map yet (data through 14 Oct 2026).
- Builds on 7 of its 48 references that are in the map.
- First posted on arXiv 11 May 2026.

## Builds on (most cited first, 7 of 7)

- [nl2spec: Interactively Translating Unstructured Natural Language to Temporal Logics with Large Language Models](https://mlsanity.com/paper/2303.04864/) (2023)
- [Formal Specifications from Natural Language](https://mlsanity.com/paper/2206.01962/) (2022)
- [Specification Patterns for Robotic Missions](https://mlsanity.com/paper/1901.02077/) (2019)
- [Model-checking in the Foundations of Algorithmic Law and the Case of Regulation 561](https://mlsanity.com/paper/2307.05658/) (2023)
- [A Compositional Proof Framework for FRETish Requirements](https://mlsanity.com/paper/2201.03641/) (2022)
- [The JKind Model Checker](https://mlsanity.com/paper/1712.01222/) (2017)
- [Controlled Natural Languages and Default Reasoning](https://mlsanity.com/paper/1905.04422/) (2019)

## Abstract (arXiv)

Formalisation is the process of writing system requirements in a formal language. These requirements mostly originate in Natural Language. In the field of Formal Methods, formalisation is often identified as one of the most delicate and complicated steps in the verification process. Not seldomly, formalisation tools and environments choose various levels of requirement descriptions: Natural Language, Technical Language, Diagram Representations and Formal Language, to mention a few. In the literature, there are various maxims and principles of good practice to guide the process of requirement formalisation. In this paper we propose a new guideline: Coherency through Formalisations. The guideline states that the different levels of formalisation mentioned above should roughly follow the same logical structure. The principle seems particularly relevant in the setting where LLMs are prompted to perform reasoning tasks that can be checked by formal tools using Structured Natural Language to act as an intermediate layer bridging both paradigms. In the light of coherency, we analyze NASA's Formal Requirement Elicitation Tool FRET and propose an alternative automated translation of the Controlled Natural Language FRETish to the formal language of MTL. We compare our translation to the original translation and prove equivalence using model checking. Some statistics are performed which seem to favor the new translation. As expected, the translation process yielded interesting reflections and revealed inconsistencies which we present and discuss.