<p>Informal specifications of software artefacts need to be formalised to facilitate rigorous analysis, including deductive verification. Automated formalisation of informal specifications can significantly reduce the effort of manual translation. However, a major challenge lies in bridging the gap between the rich syntax of natural language and the need for precise semantics in formal specification languages. Building on the empirical observation that modern pre-trained large language models (LLMs) can effectively handle the breadth of natural language, while symbolic natural language processing (NLP) is more efficient in formal languages, this paper proposes an approach that combines both methodologies. The proposed solution, Hybrid Automated Formalisation of Informal Specifications (HAFIS), uses an LLM to restrict the syntax of informal specifications into the language of a formal grammar, and proposes the concept of Typed Semantic Interpretation to enforce the semantics of the resulting formal specifications. Using a public set of real-world informal specifications, we evaluated HAFIS and compared it with a purely symbolic approach and the direct use of LLMs as baselines. Results show that HAFIS increases language acceptance from 23% to 100% and accurately translates 88% of the cases into Java Modeling Language (JML). Furthermore, mutation analysis shows that the HAFIS-generated JML effectively finds defects in programs. These results substantiate that the proposed approach is effective and contributes to software analysis using natural language.</p>