The field of software development is witnessing a significant shift towards the integration of formal methods and large language models (LLMs) to improve the quality and efficiency of the development process. This trend is driven by the need for more accurate and comprehensive software specifications, as well as the potential for automated verification and validation of software artifacts. Researchers are exploring the use of LLMs to generate formal specifications, auto-document code, and validate textual constraints against formal models. The integration of formal methods and LLMs is expected to enhance the readability and interpretability of software designs, facilitating the transition from design to implementation. Noteworthy papers in this area include:

• A study on auto-documenting JML Java code, which demonstrates the effectiveness of formal specifications in improving documentation quality.
• A framework for integrating LLMs and formal verification in the requirements engineering phase, which enables the automatic generation of program skeletons.
• A research effort towards bridging formal methods and human interpretability, which identifies key metrics for evaluating the comprehensibility of labeled transition systems.