Formal Verification of Transcompiled Mobile Applications Using First-Order Logic

Abstract

The increasing interest in automated code conversion and transcompilation—driven by the need to support multiple platforms efficiently—has raised new challenges in verifying that translated codes preserve the intended behaviors of the originals. Although it has not yet been widely adopted, transcompilation offers promising applications in software reuse and cross-platform migration. With the growing use of Large Language Models (LLMs) in code translation, where internal reasoning remains inaccessible, verifying the equivalence of their generated outputs has become increasingly essential. However, existing evaluation metrics—such as BLEU and CodeBLEU, which are commonly used as baselines in transcompiler evaluation—primarily measure syntactic similarity, even though this does not guarantee semantic correctness. This syntactic bias often leads to misleading evaluations where structurally different but semantically equivalent code is penalized. This syntactic bias often leads to misleading evaluations, where structurally different but semantically equivalent code is penalized. To address this limitation, we propose a formal verification framework based on equivalence checking using First-Order Logic (FOL). The approach models core programming constructs—such as loops, conditionals, and function calls—that function as logical axioms, enabling equivalence to be assessed at the behavioral level rather than simply by their textual similarity. We initially used the Z3 solver to manually encode Swift and Java code into FOL. To improve scalability and automation, we later integrated ANTLR to parse and translate both the source and transcompiled codes into logical representations. Although the framework is language-agnostic, we demonstrate its effectiveness through a case study of Swift-to-Java transcompilation. The experimental results demonstrated that our method effectively identifies semantic equivalence, even when syntax differs significantly. Our method achieves an average semantic accuracy of 86.1%, compared to BLEU’s syntactic accuracy of 64.45%. This framework bridges the gap between code translation and formal semantic verification. These results highlight the potential for formal equivalence checking to serve as a more reliable validation method in code translation tasks, enabling more trustworthy cross-language code conversion.