mcp-server-py2many

A Model Context Protocol (MCP) server that provides tools for transpiling Python code to multiple programming languages using py2many.

Overview

This MCP server exposes tools that allow LLMs to transpile Python code to various target languages including C++, Rust, Go, Kotlin, Dart, Julia, Nim, V, Mojo, D, SMT, and Zig.

Installation

Using uv (recommended)

# Clone the repository
git clone <repository-url>
cd mcp-server-py2many

# Install dependencies
uv sync

# Run the server
uv run mcp-server-py2many

Using pip

pip install mcp-server-py2many

Configuration

Add this server to your MCP client configuration:

Claude Desktop Config

Add to your claude_desktop_config.json:

{
  "mcpServers": {
    "py2many": {
      "command": "uvx",
      "args": ["mcp-server-py2many"]
    }
  }
}

Or with a local installation:

{
  "mcpServers": {
    "py2many": {
      "command": "uv",
      "args": ["run", "--directory", "/path/to/mcp-server-py2many", "mcp-server-py2many"]
    }
  }
}

Available Tools

1. transpile_python

Transpile Python code to another programming language using deterministic rules-based translation.

Parameters:

• python_code (string, required): The Python code to transpile
• target_language (string, required): Target language (cpp, rust, go, kotlin, dart, julia, nim, vlang, mojo, dlang, smt, zig)

2. transpile_python_with_llm

Transpile Python code using py2many with LLM assistance for better handling of complex idioms.

Parameters:

• python_code (string, required): The Python code to transpile
• target_language (string, required): Target language (cpp, rust, go, kotlin, dart, julia, nim, vlang, mojo, dlang, smt, zig)

3. list_supported_languages

List all supported target languages for transpilation.

4. verify_python

Verify Python code using SMT and z3 solver. This tool transpiles Python code using the --smt flag and then verifies it via z3 to check that the inverse of the pre/post conditions are unsat.

Parameters:

• python_code (string, required): The Python code to verify

How it works:

1. Transpiles Python code to SMT-LIB format using py2many --smt
2. Extracts preconditions from the generated SMT (functions ending in -pre)
3. Constructs a verification query that checks if there's a counterexample where:
   • The preconditions hold (valid inputs)
   • The implementation differs from the specification
4. Runs z3 on the verification query
5. Returns SAT if a bug/counterexample is found, UNSAT if verified

Example: Triangle Classification Bug Detection

This example uses the triangle_buggy.py test case from py2many to detect a bug in the triangle classification implementation:

from adt import adt as sealed

from py2many.smt import check_sat, default_value, get_model
from py2many.smt import pre as smt_pre


@sealed
class TriangleType:
    EQUILATERAL: int
    ISOSCELES: int
    RIGHT: int
    ACUTE: int
    OBTUSE: int
    ILLEGAL: int


a: int = default_value(int)
b: int = default_value(int)
c: int = default_value(int)


def classify_triangle_correct(a: int, b: int, c: int) -> TriangleType:
    """Correct implementation that properly sorts sides before classification"""
    if a == b and b == c:
        return TriangleType.EQUILATERAL
    elif a == b or b == c or a == c:
        return TriangleType.ISOSCELES
    else:
        if a >= b and a >= c:
            if a * a == b * b + c * c:
                return TriangleType.RIGHT
            elif a * a < b * b + c * c:
                return TriangleType.ACUTE
            else:
                return TriangleType.OBTUSE
        elif b >= a and b >= c:
            if b * b == a * a + c * c:
                return TriangleType.RIGHT
            elif b * b < a * a + c * c:
                return TriangleType.ACUTE
            else:
                return TriangleType.OBTUSE
        else:
            if c * c == a * a + b * b:
                return TriangleType.RIGHT
            elif c * c < a * a + b * b:
                return TriangleType.ACUTE
            else:
                return TriangleType.OBTUSE


def classify_triangle(a: int, b: int, c: int) -> TriangleType:
    """Buggy implementation - assumes a >= b >= c without sorting"""
    # Pre-condition: all sides must be positive and satisfy triangle inequality
    if smt_pre:
        assert a > 0
        assert b > 0
        assert c > 0
        assert a < (b + c)

    if a >= b and b >= c:
        if a == c or b == c:
            if a == b and a == c:
                return TriangleType.EQUILATERAL
            else:
                return TriangleType.ISOSCELES
        else:
            # BUG: Not sorting sides, assuming a is largest
            if a * a != b * b + c * c:
                if a * a < b * b + c * c:
                    return TriangleType.ACUTE
                else:
                    return TriangleType.OBTUSE
            else:
                return TriangleType.RIGHT
    else:
        return TriangleType.ILLEGAL


# Assert that the buggy version differs from correct version
assert not classify_triangle_correct(a, b, c) == classify_triangle(a, b, c)
check_sat()
get_model()

Verification Result:

=== z3 verification result ===
sat
(
  (define-fun a () Int
    1)
  (define-fun c () Int
    2)
  (define-fun b () Int
    2)
)

=== VERIFICATION FAILED ===
SAT means a counterexample was found where the implementation differs from the spec.

The counterexample found: a=1, b=2, c=2 - this satisfies the preconditions (all positive, a < b+c) but the buggy implementation returns ILLEGAL while the correct implementation returns ISOSCELES.

Use Cases:

• Detect bugs in implementations by comparing against reference implementations
• Verify that functions meet their specifications
• Formal verification of pre/post conditions
• Finding counterexamples for incorrect algorithms

When to Use Deterministic vs LLM-Assisted Translation

Use Deterministic Translation (transpile_python) when:

✅ Simple, idiomatic Python code

• Basic control flow (if/else, for/while loops)
• Standard library functions with direct equivalents
• Data structures (lists, dicts, sets)
• Simple functions and classes

✅ Well-tested patterns

• Mathematical computations
• String manipulations
• File I/O operations
• Algorithmic implementations

✅ When reproducibility matters

• Same input always produces same output
• No external dependencies or API calls
• Clear, deterministic behavior

Example cases for deterministic:

# Simple functions
def factorial(n):
    if n <= 1:
        return 1
    return n * factorial(n - 1)

# Data processing
def sum_even_numbers(numbers):
    return sum(n for n in numbers if n % 2 == 0)

# Basic algorithms
def binary_search(arr, target):
    left, right = 0, len(arr) - 1
    while left <= right:
        mid = (left + right) // 2
        if arr[mid] == target:
            return mid
        elif arr[mid] < target:
            left = mid + 1
        else:
            right = mid - 1
    return -1

Use LLM-Assisted Translation (transpile_python_with_llm) when:

🧠 Complex Python idioms

• Decorators and metaclasses
• Complex comprehensions with multiple clauses
• Generator expressions and coroutines
• Dynamic typing patterns

🧠 Language-specific features need translation

• Python-specific libraries (numpy, pandas patterns)
• Duck typing and protocol implementations
• Monkey patching and runtime modifications
• Context managers with complex behavior

🧠 Deterministic translation fails or produces non-idiomatic code

• Type errors that need semantic understanding
• Non-idiomatic output in target language
• Missing imports or dependencies
• Complex inheritance patterns

🧠 Target language best practices differ significantly

• Rust ownership and borrowing patterns
• C++ memory management
• Go concurrency patterns
• Functional programming in target language

Example cases for LLM-assisted:

# Complex decorators
def memoize(func):
    cache = {}
    def wrapper(*args):
        if args not in cache:
            cache[args] = func(*args)
        return cache[args]
    return wrapper

# Complex data transformations
def process_data(data):
    return [
        {
            'name': item['name'].upper(),
            'values': [x * 2 for x in item['values'] if x > 0]
        }
        for item in data
        if item.get('active') and len(item.get('values', [])) > 5
    ]

# Dynamic behavior
class DynamicClass:
    def __getattr__(self, name):
        return lambda *args: f"Called {name} with {args}"

Decision Flowchart

Is your Python code...
│
├─ Simple functions/algorithms?
│  └─ Yes → Use deterministic ✓
│
├─ Standard data structures and control flow?
│  └─ Yes → Use deterministic ✓
│
├─ Complex decorators, metaclasses, dynamic behavior?
│  └─ Yes → Use LLM-assisted 🧠
│
├─ Heavy use of Python-specific idioms?
│  └─ Yes → Use LLM-assisted 🧠
│
├─ Did deterministic translation fail?
│  └─ Yes → Try LLM-assisted 🧠
│
└─ Need idiomatic target language output?
   └─ Yes → Use LLM-assisted 🧠

Supported Languages

Language	Code	Notes
C++	cpp	Full support with STL containers
Rust	rust	Ownership-aware translation
Go	go	Idiomatic Go code generation
Kotlin	kotlin	JVM-compatible output
Dart	dart	Flutter-friendly
Julia	julia	Scientific computing focus
Nim	nim	Systems programming
V	vlang	Simple, fast compilation
Mojo	mojo	AI/ML performance computing
D	dlang	Systems programming
Zig	zig	Modern systems programming

Design by Contract with SMT

SMT (Satisfiability Modulo Theories) support in py2many enables Design by Contract programming—writing specifications that can be formally verified using Z3 or other SMT solvers. Unlike other target languages, SMT output is not meant to be a direct end-user programming language, but rather a specification language for verification.

Key Concepts:

• Pre-conditions: Constraints that must hold before a function executes
• Post-conditions: Constraints that must hold after a function executes
• Refinement types: Types with additional constraints (e.g., int where 1 < x < 1000)

Example: Mathematical Equations with Constraints

Python source with pre-conditions:

from py2many.smt import check_sat, default_value, get_value
from py2many.smt import pre as smt_pre

x: int = default_value(int)
y: int = default_value(int)
z: float = default_value(float)


def equation(x: int, y: int) -> bool:
    if smt_pre:
        assert x > 2        # pre-condition
        assert y < 10       # pre-condition
        assert x + 2 * y == 7  # constraint equation
    True


def fequation(z: float) -> bool:
    if smt_pre:
        assert 9.8 + 2 * z == z + 9.11
    True


assert equation(x, y)
assert fequation(z)
check_sat()
get_value((x, y, z))

Generated SMT-LIB 2.0 output:

(declare-const x Int)
(declare-const y Int)
(declare-const z Real)

(define-fun equation-pre ((x Int) (y Int)) Bool
  (and
    (> x 2)
    (< y 10)
    (= (+ x (* 2 y)) 7)))

(define-fun equation ((x Int) (y Int))  Bool
  true)

(assert (and
          (equation-pre  x y)
          (equation x y)))

(check-sat)
(get-value (x y z))

When run with z3 -smt2 equations.smt, the solver proves the constraints are satisfiable and returns values: x = 7, y = 0, z = -0.69.

Use Cases:

• Static verification: Prove correctness before deployment
• Refinement types: Enforce range constraints on integers (e.g., UserId must be 0 < id < 1000)
• Protocol verification: Ensure state machines follow valid transitions
• Security properties: Verify input sanitization pre-conditions

Further Reading:

• PySMT: Design by Contract in Python - How py2many enables refinement types and formal verification
• Agentic Transpilers - Architecture for multi-level transpilation with verification
• equations.py source - Python test case
• equations.smt output - Generated SMT-LIB

Examples

Example 1: Simple Function (Deterministic)

# Python input
def greet(name):
    return f"Hello, {name}!"

# C++ output (via transpile_python)
#include <iostream>
#include <string>

std::string greet(std::string name) {
    return "Hello, " + name + "!";
}

Example 2: Complex Data Processing (LLM-Assisted)

# Python input with complex comprehensions
def analyze_sales(data):
    return {
        region: {
            'total': sum(s['amount'] for s in sales),
            'count': len(sales),
            'avg': sum(s['amount'] for s in sales) / len(sales)
        }
        for region, sales in data.items()
        if any(s['amount'] > 1000 for s in sales)
    }

# Better results with LLM-assisted translation for idiomatic target language

Development

# Install development dependencies
uv sync

# Run the server
uv run mcp-server-py2many

# Test the server manually
uv run python -m mcp_server_py2many

How It Works

1. The MCP server receives a request with Python code and target language
2. Creates a temporary Python file with the code
3. Runs py2many --{language} (or with --llm flag) on the file
4. Captures the generated output and any errors
5. Returns the transpiled code to the LLM client

Limitations

• Not all Python features are supported in all target languages
• Some Python standard library functions may not have direct equivalents
• Complex dynamic Python code may require manual adjustments after transpilation
• LLM-assisted mode requires an LLM API key configured for py2many

License

MIT License - See LICENSE file for details.

Contributing

Contributions welcome! Please open issues and pull requests on the repository.

Related Projects

• py2many - The transpiler this MCP server wraps
• MCP - Model Context Protocol specification