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

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

Problem Statement
The integration of novel medical devices into existing Medical Internet of Things (MIoT) networks presents significant challenges, particularly when human software development expertise is unavailable. While Large Language Models (LLMs) offer powerful code synthesis capabilities, they are prone to hallucinations and subtle vulnerabilities, making them unreliable for safety-critical healthcare domains. The core problem addressed is the need to automatically generate trustworthy, reliable translation code that converts data from device-specific formats (e.g., custom JSON schemas) into standardized interoperability formats (e.g., Fast Healthcare Interoperability Resources or FHIR) without manual verification, which is often intractable at scale.

Methodology
The authors propose a neuro-symbolic architecture that integrates LLMs with formal verification to synthesize correct-by-construction code. The system is built upon ShinkaEvolve, an open-source evolutionary code optimization framework. The pipeline operates as follows:

1. Evolutionary Search with LLMs: The system employs a multi-island evolutionary algorithm where LLMs act as operators. Instead of random mutations, LLMs propose semantically meaningful program edits, rewrites, or mutations based on a prompt containing parent programs, "inspiration" programs, and their fitness scores.
2. Formal Verification as Fitness Function: To ensure reliability, the system uses the Prototype Verification System (PVS), a theorem prover, as the evaluator. The LLM is tasked with generating a translation theorem in PVS's Domain-Specific Language (DSL) that maps an input JSON schema to an output JSON schema.
   • The fitness function is binary: a candidate program receives a score of 1 if the PVS theorem prover verifies the translation is correct (i.e., all valid inputs map to valid outputs satisfying the target schema), and 0 otherwise.
   • To mitigate the LLM's limited familiarity with PVS, the prompt includes a language reference and in-context examples of simple schema translations.
3. Code Generation: Once a theorem is formally verified, the system utilizes additional tooling to deterministically transform the verified PVS theorem into executable C code, suitable for deployment within the resource-constrained MIoT environment.

Key Contributions

• Neuro-Symbolic Pipeline: The integration of an LLM-driven evolutionary search with a formal theorem prover (PVS) to guarantee that synthesized code satisfies strict structural requirements.
• MIoT Case Study: A practical demonstration of integrating a pulse oximeter into a vehicle-based MIoT network. The system successfully translates the device's custom JSON schema into the standard FHIR Observation resource format.
• Low-Cost Reliability: The demonstration that formally verified code can be generated consistently with low computational and financial overhead.

Experimental Results
The authors conducted 10 independent experimental runs, each consisting of 20 generations across two evolutionary islands, to analyze the integration of the pulse oximeter.

• Success Rate: The system achieved a success rate of 37.4% ± 22.4% (the fraction of LLM-generated programs that passed verification).
• Efficiency: The earliest successful theorem was found on average at Generation 5.0. The average time to find the first successful program was 10.4 minutes, with a total wall-clock time of 42.7 minutes per experiment.
• Cost: The average total API cost per experiment was $0.87. Crucially, the cost incurred before finding the first successful proof was only $0.18 (approx. 20% of the total budget).
• Model Performance: An ensemble of models (GPT-5, GPT-5-mini, o4-mini, GPT-5-nano) was used with dynamic weighting via Thompson sampling. GPT-5 accounted for 33.7% of selections but generated 53.5% of successful programs, indicating that larger models were more effective at generating correct PVS theorems.
• Convergence: Despite varying LLM selection paths and intermediate failures, all 10 experiments converged to semantically identical solutions, suggesting the formal constraints of the FHIR schema are highly prescriptive.

Significance and Claims
The paper positions this work as a "first step" toward the trustworthy automatic integration of novel devices into existing healthcare infrastructure. The authors claim that their system demonstrates the feasibility of generating formally verified translation code at a low cost, ensuring that structured data translated by the generated code will always conform to the target output schema.

The significance lies in addressing the safety-critical nature of healthcare systems by grounding the reasoning power of LLMs in formal verification, thereby mitigating the risks of hallucination and ensuring reliability without requiring human software development expertise. The authors explicitly state that future work will involve expanding the device set, verifying networking components, and integrating this verification stage into a fully agentic pipeline.