PolyVer: A Compositional Approach for Polyglot System Modeling and Verification

Basic Information

• Paper ID: 2503.03207
• Title: PolyVer: A Compositional Approach for Polyglot System Modeling and Verification
• Authors: Pei-Wei Chen, Shaokai Lin, Adwait Godbole, Ramneet Singh, Elizabeth Polgreen, Edward A. Lee, Sanjit A. Seshia
• Classification: cs.PL (Programming Languages)
• Publication Venue/Conference: Formal Methods in Computer-Aided Design 2025
• Paper Link: https://arxiv.org/abs/2503.03207

Abstract

Polyglot software systems are composed of programs implemented in multiple programming languages, yet existing program verifiers are typically tailored to single languages. To verify polyglot systems, translation to a common verification language or formal representation is usually required. This paper proposes PolyVer, an alternative approach that performs polyglot verification directly using abstraction, compositional reasoning, and synthesis techniques. PolyVer models polyglot systems as formal transition systems where transition-related update functions are implemented in target languages (such as C or Rust). To perform verification, PolyVer connects a model checker for transition systems with language-specific verifiers through pre/post-condition contracts on update functions. These contracts are automatically generated through synthesis oracles based on syntax-guided synthesis or large language models, and are checked by language-specific verifiers.

Research Background and Motivation

Problem Definition

Modern software systems increasingly adopt polyglot architectures, where frameworks like ROS2 and Lingua Franca allow developers to select the most suitable programming language for different components. However, this flexibility introduces verification challenges:

1. Language Semantic Differences: Different programming languages have distinct syntax and semantics. For example, Rust's saturating_add function saturates to the maximum value on overflow, while C addition may wrap around.
2. Limitations of Existing Verifiers: Most program verifiers (such as CBMC for C, Kani for Rust) are specifically designed for single languages and cannot directly handle polyglot systems.
3. Translation Complexity: Translating an entire polyglot system to a single verification language requires supporting the complete syntax and semantics of all languages, which is prohibitive for modern languages.

Research Significance

The increased complexity of polyglot systems raises the risk of software defects. In safety-critical domains (such as autonomous driving and aerospace), formal verification provides stronger guarantees than incomplete methods like testing alone.

Limitations of Existing Approaches

• Monolithic Translation Methods: Require developing complete compiler infrastructure for each language
• Semantic Preservation Difficulty: Challenging to faithfully capture all language-specific constructs from source languages in target verification languages
• Scalability Issues: Generated verification problems may become prohibitively large

Core Contributions

1. Formalization of Polyglot Verification Problem: First systematic formalization of the polyglot verification problem and proposes a compositional solution integrating multiple language-specific verifiers.
2. Automated Contract Synthesis: Proposes automatic synthesis and refinement of pre/post-condition contracts using intermediate languages and CEGIS-CEGAR loops, supporting both syntax-guided synthesis and large language models as synthesis oracles.
3. Tool Implementation: Implements PolyVer tool based on UCLID5, supporting C and Rust through CBMC and Kani verifiers, demonstrating that LLM-based synthesis oracles outperform pure symbolic synthesis methods.
4. Case Studies and Evaluation: Develops a verifier for the Lingua Franca coordination language, verifies polyglot systems containing C and Rust processes, and handles C language fragments that previous work could not support.

Methodology Details

Task Definition

Input: Polyglot model M = (Q,V,I₀,T,F) and system property φ Output: Verification result (pass/fail) and possible counterexample trace Objective: Determine whether M ⊨ φ holds

Where:

• Q: Set of modes
• V: Set of typed variables
• I₀: Set of initial states
• T: Set of mode transitions
• F: Set of procedures

Model Architecture

1. Extended State Machine (ESM)

PolyVer models polyglot systems as extended state machines where:

• States consist of modes and variable assignments
• Transitions are associated with guard conditions and update relations
• Update relations specialize into procedure call sequences

2. Intermediate Contract Language L*

A key innovation is introducing intermediate language L* as "glue" between different languages:

• Contracts are written in L*
• Transformed to concrete languages through semantics-preserving compilation compL
• Avoids complexity of complete language translation

3. CEGIS-CEGAR Hybrid Method

The algorithm core consists of two-layer iterative loops:

Outer CEGAR Loop:

1. Construct abstract model M' using current contracts
2. Model checker verifies M' ⊨ φ
3. If verification fails, check whether counterexample is spurious
4. If spurious, refine contracts; otherwise report genuine counterexample

Inner CEGIS Loop:

1. Synthesis oracle generates candidate contracts
2. Verification oracle checks contract validity
3. If invalid, add positive examples and re-synthesize

Technical Innovations

1. Compositional Verification Strategy

Unlike monolithic translation, PolyVer adopts a "divide-and-conquer" strategy:

• Use contracts to abstract individual procedures
• Language-specific verifiers verify contract validity
• Model checker verifies system-level properties

2. Automated Contract Generation

Supports multiple synthesis oracles:

• LLM-based Synthesizer: Uses chain-of-thought prompting and Python DSL
• SyGuS/SyMO Synthesizer: Encodes problems as syntax-guided synthesis problems

3. Spuriousness Checking

Distinguishes genuine counterexamples from spurious ones by verifying {V = d} C {V' ≠ d'} to check reachability of counterexample traces.

Experimental Setup

Dataset

1. LFVerifier Benchmark: 22 Lingua Franca programs with restricted C syntax
2. Complete LF Examples: LED controller, climbing robot, satellite attitude controller, and other embedded systems
3. Polyglot Systems: C/Rust mixed LF programs, ROS2 applications, FFI cross-language call programs

Evaluation Metrics

• Number of synthesis iterations (IS: CEGIS iterations, AR: CEGAR iterations)
• Runtime (SOT: synthesis oracle time, VOT: verification oracle time, UT: UCLID5 time)
• Verification success rate

Comparison Methods

Compared with LFVerifier15, the only known end-to-end automated LF program verification tool.

Implementation Details

• OpenAI o1-mini as LLM synthesizer with 3 parallel queries per procedure
• CBMC-6.3.1, Kani-0.56.0, z3-4.8.7 as verification backends
• 3.7GHz Intel Core i9 machine with 62GB RAM

Experimental Results

Main Results

RQ1: Comparison with Existing LF Verification Work

On 22 benchmark tests:

• PolyVer successfully verifies all benchmarks; LFVerifier fails on TrafficLight example
• 18 benchmarks synthesize contracts correctly in single CEGIS iteration, averaging 37 seconds
• Although total runtime is slower (primarily dominated by contract synthesis time), provides significant qualitative improvements

RQ2: Handling Complete LF Examples

Successfully verifies embedded systems with complete C code:

• LED Controller: 1 procedure, 123 lines of C code, 31.0 seconds synthesis time
• Climbing Robot: 12 procedures, 75 lines of C/Rust code, 685.4 seconds synthesis time
• Satellite Controller: 6 procedures, 424 lines of C code, 729.0 seconds synthesis time

RQ3: Polyglot System Verification

Verifies genuinely polyglot systems:

• C/Rust mixed LF programs
• ROS2 service applications
• FFI cross-language call programs

Key Findings

1. LLM Outperforms Symbolic Methods: SyGuS/SyMO solvers require numerous CEGAR iterations and frequently fail to terminate
2. Contract Synthesis Challenges: Procedures with complex control flow and data dependencies require more iterations
3. Practical Validation: Can handle real implementation code rather than toy examples

Related Work

Polyglot System Verification

• Manual Translation Methods: Cook et al. translated assembly code to C to verify Xen virtual machine monitor
• Automatic Fragment Translation: LFVerifier automatically translates C fragments to verification languages
• Black-box Methods: Infer summaries from input-output behavior

Compositional Verification

• Compositional verification based on Hoare logic widely applied to large-scale single-language programs
• Automated pre/post-condition learning using abstract interpretation and CEGAR

Contract Inference

• Property-directed contract inference methods
• Constrained Horn clause solvers
• Recent applications of LLMs in specification learning

Conclusions and Discussion

Main Conclusions

1. PolyVer successfully addresses key challenges in polyglot system verification
2. Compositional approach avoids complexity of complete language translation
3. Automated contract synthesis makes the method practical
4. LLM-based synthesizers outperform traditional symbolic methods

Limitations

1. Termination: Algorithm does not guarantee termination, depends on synthesis oracle quality
2. Language Support: Currently supports only C and Rust; requires developing verification oracles for other languages
3. Contract Expressiveness: Expressiveness of intermediate language L* limits complexity of verifiable properties
4. Scalability: Contract synthesis time for large systems may become a bottleneck

Future Directions

1. Extend to other polyglot distributed software systems and robotic software systems
2. Apply to formal verification of code translation (e.g., C to Rust translation)
3. Improve efficiency and accuracy of contract synthesis
4. Support more complex temporal logic properties

In-Depth Evaluation

Strengths

1. Problem Importance: Polyglot system verification is a practical and important problem
2. Methodological Innovation: Combination of compositional verification and automated contract synthesis is novel
3. Theoretical Foundation: Clear formal definitions with explicit correctness guarantees
4. Practical Value: Handles real systems rather than toy examples
5. Tool Implementation: Provides usable tool implementation

Weaknesses

1. Performance Overhead: Contract synthesis time is lengthy, potentially limiting practical applications
2. Language Coverage: Currently supports only C and Rust; extensibility remains to be verified
3. Limited Benchmarks: While including real examples, scale is relatively small
4. LLM Dependency: Relies on commercial LLM services, potentially affecting reproducibility

Impact

1. Academic Contribution: Opens new research direction for polyglot system verification
2. Practical Value: Provides verification tools for safety-critical polyglot systems
3. Technical Inspiration: Idea of contracts as language interfaces has universal value

Applicable Scenarios

1. Embedded Systems: Real-time systems mixing C/Rust
2. Distributed Systems: ROS2, gRPC, and other polyglot frameworks
3. Safety-Critical Applications: Systems requiring formal verification guarantees
4. Legacy System Integration: Systems mixing old and new code

References

The paper cites 50 related works covering multiple domains including polyglot systems, formal verification, contract inference, and syntax-guided synthesis, providing solid theoretical foundation for the research.

Overall Assessment: This is a high-quality systems research paper addressing an important and practical problem. The methodology is innovative, experiments are comprehensive, and tool implementation is complete. While there is room for improvement in performance and scalability, it makes significant contributions to the polyglot system verification field.