Formally Verified Code Synthesis for Structured Data Translation in a Medical Internet of Things

This article presents a code synthesis system that leverages a large language model (LLM) for structured data translation in Medical Internet of Things applications, specifically focusing on integrating a pulse oximeter into an existing network. The system incorporates a formal verification step to ensure that the generated code adheres to predefined requirements, enabling reliable translation between the device's JSON schema and the Fast Healthcare Interoperability Resources (FHIR) format. Experimental results indicate that the system consistently produces correct translations at a low cost, highlighting its potential for practitioners needing trustworthy code generation in healthcare settings.