# Lean Proof To Code Translator - C Rust Wasm

## Links

- Product page URL: https://www.agentpmt.com/marketplace/lean-to-code-translator-w-proof-c-rust-wasm
- Product markdown URL: https://www.agentpmt.com/marketplace/lean-to-code-translator-w-proof-c-rust-wasm?format=agent-md
- Product JSON URL: https://www.agentpmt.com/marketplace/lean-to-code-translator-w-proof-c-rust-wasm?format=agent-json

## Overview

- Product ID: 69cdb31aff055c86b8b8a224
- Type: function
- Unit type: request
- Price: 500 credits
- Categories: Scientific Computing, Developer Tools, Compliance & Audit, Testing & QA, Data Processing, Data Validation & Verification, File & Binary Operations
- Generated at: 2026-07-05T04:09:53.796Z

### Page Description

The Lean to Code Translator converts exportable Lean proof programs into auditable C, Rust, or WebAssembly deliverables. Upload a Lean source bundle, choose the entry module and symbol, and get generated code plus a certificate, logs, and a verification bundle so you can preserve provenance, re-run validation, and confirm the artifact still matches the original source under the pinned runtime.

### Agent Description

Start asynchronous Lean proof export and verification jobs, list supported export targets, check individual task status, list recent tasks, and retrieve generated bundle, certificate, log, and output file metadata when a task completes.

## Details

### Details

The Lean to Code Translator converts exportable Lean proof programs into auditable C, Rust, or WebAssembly deliverables. Upload a Lean source bundle, choose the entry module and symbol, and get generated code plus a certificate, logs, and a verification bundle so you can preserve provenance, re-run validation, and confirm the artifact still matches the original source under the pinned runtime.

### Actions

- `generate` (5 credits): Compile a source-only Lean archive into verified C, Rust, or Wasm artifacts using the platform-pinned runtime and shared cache. This action starts an asynchronous task and returns a task_id immediately.
- `verify` (5 credits): Verify a previously generated Lean proof export bundle against the same pinned runtime and shared cache. This action starts an asynchronous task and returns a task_id immediately.
- `get_targets` (5 credits): List the currently supported target languages and bundle requirements.
- `get_task` (5 credits): Check the status of a generate or verify task and retrieve results when complete.
- `list_tasks` (5 credits): List recent generate and verify tasks for the current budget.

### Use Cases

Compile Lean proof programs to C for native integration, Generate Rust exports from pinned Lean proof bundles, Produce constrained Wasm artifacts from Lean proof code, Package code generation runs with certificates and logs, Verify previously generated bundles before shipping or publication, Preserve reproducible build evidence for audits and reviews, Archive proof export bundles for downstream teams

### Workflows Using This Tool

No public workflows currently reference this product.

### Related Content

#### AI Compliance Regulations: Verified Lean Proofs to Code

- Type: article
- Page URL: https://www.agentpmt.com/articles/ai-compliance-regulations-verified-lean-proofs-to-code
- Markdown URL: https://www.agentpmt.com/articles/ai-compliance-regulations-verified-lean-proofs-to-code?format=agent-md
AgentPMT now offers the Lean Proof To Code Translator from Apoth3osis, a managed connector that compiles exportable Lean proofs into auditable C, Rust, or Wasm with a certificate, build logs, and a verification bundle. Agents generate and re-verify reproducible, audit-ready artifacts pay-per-use through AgentPMT's dynamic MCP server.

## Integration Details

### DynamicMCP

- Setup page URL: https://www.agentpmt.com/dynamic-mcp
- Claude setup guide: https://www.agentpmt.com/dynamic-mcp#platform=claude
- ChatGPT setup guide: https://www.agentpmt.com/dynamic-mcp#platform=chatgpt
- Cursor setup guide: https://www.agentpmt.com/dynamic-mcp#platform=cursor
- Windsurf setup guide: https://www.agentpmt.com/dynamic-mcp#platform=windsurf

Use the local router for command-based MCP clients. It forwards requests to `https://api.agentpmt.com/mcp` and does not execute tools locally.

```bash
npm install -g @agentpmt/mcp-router
agentpmt-setup
```

### REST API

The live page renders cURL, Python, JavaScript, and Node.js examples. Logged-in users see those examples prefilled with their own API and budget credentials.

- Purchase endpoint: https://api.agentpmt.com/products/purchase
- Authorization format: `Bearer <base64(apiKey:budgetKey)>`

```bash
curl -X POST "https://api.agentpmt.com/products/purchase" \
  -H "Content-Type: application/json" \
  -H "Authorization: Bearer eW91ci1hcGkta2V5LWhlcmU6eW91ci1idWRnZXQta2V5LWhlcmU=" \
  -d '{
    "product_id": "69cdb31aff055c86b8b8a224",
    "parameters": {
      "action": "generate"
    }
  }'
```

### Autonomous Agents

Autonomous agents can access this tool through AgentAddress credit balances or direct x402 payments. Use the Autonomous Agent API reference for endpoint shapes after choosing the access pattern below.

- Autonomous Agent API reference URL: https://www.agentpmt.com/docs/api-reference/autonomous-agents
- Autonomous Agent API reference markdown URL: https://www.agentpmt.com/docs/api-reference/autonomous-agents?format=agent-md
- Credit-Based Access Using AgentAddress: https://www.agentpmt.com/docs/autonomous-agents/credit-based-tool-usage-with-agentaddress
- AgentAddress is preferred for persistent file access, stored platform state, and maximum tool use ability across repeated calls.
- Direct x402 is for independent one-off tool calls that do not require shared files or stored platform state.
- Direct x402 public payments: USDC on Base, Arbitrum, Optimism, Polygon, and Avalanche.

#### Product Skill Package

This product has a published Agent Skill package for product-specific operating instructions.

- Skill slug: lean-proof-to-code-translator-c-rust-wasm
- Version: 1.0.1
- Download SKILL.md: https://raw.githubusercontent.com/AgentPMT/agent-skills/main/skills/lean-proof-to-code-translator-c-rust-wasm/SKILL.md
- Package source: https://github.com/AgentPMT/agent-skills/tree/main/skills/lean-proof-to-code-translator-c-rust-wasm
- OpenClaw listing: https://clawhub.ai/agentpmt/lean-proof-to-code-translator-c-rust-wasm
- OpenClaw install: `openclaw skills install lean-proof-to-code-translator-c-rust-wasm`
- skills.sh install: `npx skills add AgentPMT/agent-skills --skill lean-proof-to-code-translator-c-rust-wasm`
- Last published: 2026-06-09T23:55:11.220Z

### Schema

#### Parameters

- Schema type: actions

```json
{
  "actions": {
    "generate": {
      "description": "Compile a source-only Lean archive into verified C, Rust, or Wasm artifacts using the platform-pinned runtime and shared cache. This action starts an asynchronous task and returns a task_id immediately.",
      "properties": {
        "source_archive_file_id": {
          "type": "string",
          "description": "Stored zip archive containing Lean source files under UserProofs/. Do not upload lakefile.lean, lean-toolchain, lake-manifest.json, or .lake.",
          "required": false
        },
        "use_vendored_runtime": {
          "type": "boolean",
          "description": "When true, generate from the vendored Lean runtime shipped in the isolated lean-service container.",
          "required": false
        },
        "entry_module": {
          "type": "string",
          "description": "Lean module to import from the uploaded source tree, for example UserProofs.Main.",
          "required": false
        },
        "entry_symbol": {
          "type": "string",
          "description": "Lean definition to export from entry_module. Fully qualified names are accepted; unqualified names are tried as bare names and common namespace-qualified forms.",
          "required": false
        },
        "target_language": {
          "type": "string",
          "description": "Target language to generate. Supported values: c, rust, wasm.",
          "required": false,
          "enum": [
            "c",
            "rust",
            "wasm"
          ]
        },
        "timeout_seconds": {
          "type": "integer",
          "description": "How long to wait for the isolated lean-service request before failing.",
          "required": false,
          "minimum": 10,
          "maximum": 300
        }
      }
    },
    "verify": {
      "description": "Verify a previously generated Lean proof export bundle against the same pinned runtime and shared cache. This action starts an asynchronous task and returns a task_id immediately.",
      "properties": {
        "bundle_file_id": {
          "type": "string",
          "description": "Stored bundle zip file_id produced by a previous generate call.",
          "required": true
        },
        "target_language": {
          "type": "string",
          "description": "Target language encoded in the bundle. Supported values: c, rust, wasm.",
          "required": false,
          "enum": [
            "c",
            "rust",
            "wasm"
          ]
        },
        "verification_mode": {
          "type": "string",
          "description": "Use fast for hash checks or full to rebuild and re-export.",
          "required": false,
          "enum": [
            "fast",
            "full"
          ]
        },
        "timeout_seconds": {
          "type": "integer",
          "description": "How long to wait for the isolated lean-service request before failing.",
          "required": false,
          "minimum": 10,
          "maximum": 300
        }
      }
    },
    "get_targets": {
      "description": "List the currently supported target languages and bundle requirements."
    },
    "get_task": {
      "description": "Check the status of a generate or verify task and retrieve results when complete.",
      "properties": {
        "task_id": {
          "type": "string",
          "description": "Task ID returned from a previous generate or verify call.",
          "required": true
        }
      }
    },
    "list_tasks": {
      "description": "List recent generate and verify tasks for the current budget.",
      "properties": {
        "limit": {
          "type": "integer",
          "description": "Maximum number of tasks to return. Default 20.",
          "required": false,
          "minimum": 1,
          "maximum": 100
        }
      }
    }
  }
}
```

### Usage Instructions

# Supported Lean Input For Code Generation

Full step-by-step tutorial:
- `https://www.agentpmt.com/docs/tutorials/write-lean-input-for-code-generation`

Download the working example zip:
- `https://www.agentpmt.com/downloads/lean-proof-code-generation-example.zip`

This service does not accept arbitrary Lean programs and "turn them into C".
It accepts Lean source that builds a value of:

- `HeytingLean.LeanCP.CProgramDecl`

The selected `entry_symbol` must elaborate to that type. The generated `c`,
`rust`, and `wasm` artifacts are emitted from that LeanCP intermediate
representation.

## Async Workflow

1. Call `generate` or `verify`.
2. Poll `get_task` with the returned `task_id` until `status` is `completed` or `failed`.
3. Read artifacts from the completed task result.

## What To Put In The Archive

Upload a `.zip` file whose top-level entries are Lean source files under
`UserProofs/`.

Required:

- `UserProofs/Main.lean` or another module referenced by `entry_module`
- only `.lean` files under `UserProofs/`

Do not include:

- `lakefile.lean`
- `lean-toolchain`
- `lake-manifest.json`
- `.lake/`
- external package checkouts or generated build artifacts

The platform supplies the pinned Lean toolchain and the pinned LeanCP runtime.

## Authoring Model

You can use ordinary Lean definitions to build your program value. For example,
it is fine to use:

- `namespace`, `open`, `def`, `let`
- helper functions and helper constants
- lists, tuples, and other normal Lean data needed to assemble the IR
- small amounts of proof-oriented helper code if it stays within the pinned runtime surface

What actually gets exported is only the final `CProgramDecl` value. General Lean
code is authoring support, not emitted output by itself.

## Required Export Shape

Import the LeanCP declaration and syntax modules:

```lean
import HeytingLean.LeanCP.Lang.CDecl
import HeytingLean.LeanCP.Lang.CSyntax
import HeytingLean.LeanCP.Core.HProp

open HeytingLean.LeanCP
```

Your exported symbol must be a `CProgramDecl`:

```lean
def exportProgram : CProgramDecl := {
  defs := []
  main := {
    name := "add_one"
    params := [("x", .int)]
    retType := .int
    body := .ret (.binop .add (.var "x") (.intLit 1))
  }
}
```

`CProgramDecl` contains:

- `defs : List CFunDecl`
- `main : CFunDecl`

Each `CFunDecl` contains:

- `name : String`
- `params : List (String × CType)`
- `retType : CType`
- `body : CStmt`

## Supported Type Surface

The exported IR currently supports these `CType` constructors:

- `.int`
- `.intSized signedness intSize`
- `.float`
- `.double`
- `.ptr ty`
- `.array ty n`
- `.funcPtr ret args`
- `.struct name`
- `.union name`
- `.enum name`
- `.typedef name`
- `.void`

In practice, the most stable surface today is:

- integers
- pointers
- fixed-size arrays
- the built-in struct layouts the runtime already knows about

## Supported Expression Surface

`CExpr` currently supports:

- `.var name`
- `.intLit n`
- `.floatLit v`
- `.null`
- `.sizeOf ty`
- `.cast ty expr`
- `.binop op lhs rhs`
- `.deref ptrExpr`
- `.arrayAccess arr idx`
- `.addrOf varName`
- `.fieldAccess base field`
- `.call functionName args`

Supported binary operators (`BinOp`):

- arithmetic: `.add`, `.sub`, `.mul`, `.div`, `.mod`
- comparisons: `.eq`, `.ne`, `.lt`, `.le`, `.gt`, `.ge`
- boolean/logical: `.and`, `.or`, `.lAnd`, `.lOr`
- bitwise: `.bitAnd`, `.bitOr`, `.bitXor`, `.shl`, `.shr`

## Supported Statement Surface

`CStmt` currently supports:

- `.skip`
- `.assign lhs rhs`
- `.seq s1 s2`
- `.ite cond thenStmt elseStmt`
- `.whileInv cond invariant body`
- `.block locals body`
- `.switch expr tag caseBody defaultBody`
- `.forLoop init cond step body`
- `.break`
- `.continue`
- `.ret expr`
- `.alloc varName cellCount`
- `.free expr cellCount`
- `.decl varName ty`

Useful helper:

- `switchMany expr cases defaultStmt`

Notes:

- `whileInv` takes a loop invariant of type `HProp`. Use `HProp.htrue` when you need a permissive invariant.
- `block` takes a list of local declarations as `(String × CType)`.
- `alloc` and `free` work at the LeanCP memory-model level with explicit cell counts.

## Practical Examples

Simple arithmetic function:

```lean
def applyTax : CFunDecl := {
  name := "apply_tax"
  params := [("subtotal", .int), ("tax_rate", .int)]
  retType := .int
  body := .ret
    (.binop .add
      (.var "subtotal")
      (.binop .div
        (.binop .mul (.var "subtotal") (.var "tax_rate"))
        (.intLit 100)))
}
```

Conditional return:

```lean
def shippingProgram : CProgramDecl := {
  defs := []
  main := {
    name := "shipping_quote"
    params := [("weight_kg", .int)]
    retType := .int
    body := .ite (.binop .le (.var "weight_kg") (.intLit 5))
      (.ret (.intLit 8))
      (.ret (.intLit 15))
  }
}
```

Loop with invariant:

```lean
def loyaltyProgram : CProgramDecl := {
  defs := []
  main := {
    name := "loyalty_points"
    params := [("orders", .int), ("points_each", .int)]
    retType := .int
    body := .block [("total", .int), ("i", .int)] (
      .seq (.assign (.var "total") (.intLit 0)) (
      .seq (.assign (.var "i") (.intLit 0)) (
      .seq (.whileInv (.binop .lt (.var "i") (.var "orders")) HProp.htrue (
          .seq (.assign (.var "total") (.binop .add (.var "total") (.var "points_each")))
               (.assign (.var "i") (.binop .add (.var "i") (.intLit 1)))))
          (.ret (.var "total")))))
  }
}
```

Pointer and array access:

```lean
def basketProgram : CProgramDecl := {
  defs := []
  main := {
    name := "basket_head_total"
    params := [("prices", .ptr .int)]
    retType := .int
    body := .ret (.binop .add
      (.arrayAccess (.var "prices") (.intLit 0))
      (.arrayAccess (.var "prices") (.intLit 1)))
  }
}
```

## What Will Not Work

These inputs are outside the supported contract:

- an `entry_symbol` whose type is not `CProgramDecl`
- a custom Lean package graph that depends on your own `lakefile.lean`
- imports that require packages not already present in the pinned runtime
- raw theorem statements with no executable `CProgramDecl`
- arbitrary Lean runtime code that is not expressed through the LeanCP IR

## Target Honesty

All targets start from the same `CProgramDecl`.

- `c` is the baseline and most direct emission path
- `rust` is a deterministic translation of the same C IR and uses `unsafe` for pointer semantics
- `wasm` is the most restrictive path and should be treated as preview-grade compared with `c`

### Additional Product Content

## Compile Lean proofs into auditable code artifacts

Proof Code Compiler starts asynchronous Lean proof export and verification jobs that produce reproducible **C**, **Rust**, or **WebAssembly** artifacts plus the files needed to audit and verify them later.

[Read the full Lean input tutorial](https://www.agentpmt.com/docs/tutorials/write-lean-input-for-code-generation) or [download the working example zip](https://www.agentpmt.com/downloads/lean-proof-code-generation-example.zip).

### Async workflow

1.  Call **generate** or **verify**. The tool returns a task\_id immediately.
2.  Poll **get\_task** with that task ID.
3.  When the task reaches completed, read the result payload for artifact metadata and file IDs.
4.  Use **list\_tasks** to review recent jobs for the current budget.

### What to upload for generation

Upload a .zip with a top-level UserProofs/ directory that contains only Lean source files.

```text
user_source.zip
└── UserProofs/
├── Main.lean
├── Helpers.lean
└── Submodule/Util.lean
```

Do not upload lakefile.lean, lean-toolchain, lake-manifest.json, or .lake/. The platform supplies the pinned Lean toolchain and runtime.

### Generate inputs

1.  source\_archive\_file\_id
2.  entry\_module, such as UserProofs.Main
3.  entry\_symbol, such as exportProgram
4.  target\_language: c, rust, or wasm

You may also set use\_vendored\_runtime for the built-in smoke-test program or adjust timeout\_seconds within 10-300 seconds.

### Verification inputs

Use the bundle\_file\_id from a completed generation task. Choose fast to re-check hashes and certificate details, or full to rebuild and compare regenerated output under the pinned runtime.

### Task results

Completed tasks can return generated output metadata, a verification bundle, a certificate, a generation log, and normalized source-archive metadata. Keep the bundle file ID if you want to verify the export later.

### Frequently Asked Questions

#### How do I connect this tool to an external agent?

- Page URL: https://www.agentpmt.com/faq
- Markdown URL: https://www.agentpmt.com/faq?format=agent-md

You can install the local MCP server by opening a terminal and running:

```
npm install -g @agentpmt/mcp-router
agentpmt-setup
```

This will connect you to local agents like Claude Code, Windsurf, Grok Build, Cursor, etc.

Alternatively you can connect to the hosted version with this config block, no installation required:

```
{
  "mcpServers": {
    "agentpmt": {
      "type": "streamable-http",
      "url": "https://api.agentpmt.com/mcp",
      "headers": {
        "Authorization": "Bearer <AGENTPMT_BEARER_TOKEN>",
        "x-instance-metadata": "{\"client\":\"generic-mcp\",\"platform\":\"remote\"}"
      }
    }
  }
}
```

[View MCP Connection Instructions](/docs/mcp-reference/connection) for more details.

#### How does an external agent use this tool?

- Page URL: https://www.agentpmt.com/faq
- Markdown URL: https://www.agentpmt.com/faq?format=agent-md

After the external agent is connected to an Agent Group that can use this tool, paste this prompt into the agent:

> Use the AgentPMT-Tool-Search-and-Execution tool. First call action 'get\_instructions' so you know how to use the tool search interface. Then call action 'get\_schema' with tool\_id 69cdb31aff055c86b8b8a224 ("Lean Proof To Code Translator - C Rust Wasm"). After reading the schema and any returned instructions, tell me what this tool can do, we are going to be using it

The agent should fetch the tool schema first, collect the required parameters for your request, and then call the tool through AgentPMT.

#### Can I upload `lakefile.lean`, `lean-toolchain`, or my own build configuration?

- Page URL: https://www.agentpmt.com/faq#faq-69cefe5bb1446c1c6d60b51b
- Markdown URL: https://www.agentpmt.com/faq?format=agent-md#faq-69cefe5bb1446c1c6d60b51b
- Tags: Product Specific

No. The platform pins the Lean toolchain and exporter runtime for you. Do not include \`lakefile.lean\`, \`lean-toolchain\`, \`lake-manifest.json\`, or \`.lake/\` in the uploaded archive.

#### Does this compile any Lean program?

- Page URL: https://www.agentpmt.com/faq#faq-69cefe5bb1446c1c6d60b51d
- Markdown URL: https://www.agentpmt.com/faq?format=agent-md#faq-69cefe5bb1446c1c6d60b51d
- Tags: Product Specific

No. The selected definition must elaborate to \`HeytingLean.LeanCP.CProgramDecl\`, which is the exportable LeanCP program form supported by the current compiler path.

#### What do `entry_module` and `entry_symbol` mean?

- Page URL: https://www.agentpmt.com/faq#faq-69cefe5bb1446c1c6d60b51c
- Markdown URL: https://www.agentpmt.com/faq?format=agent-md#faq-69cefe5bb1446c1c6d60b51c
- Tags: Product Specific

\`entry\_module\` is the Lean module imported from your uploaded source tree, such as \`UserProofs.Main\`. \`entry\_symbol\` is the definition exported from that module, such as \`exportProgram\`.

#### What do I upload to Proof Code Compiler?

- Page URL: https://www.agentpmt.com/faq#faq-69cefe5bb1446c1c6d60b51a
- Markdown URL: https://www.agentpmt.com/faq?format=agent-md#faq-69cefe5bb1446c1c6d60b51a
- Tags: Product Specific

Upload a \`.zip\` whose top-level folder is \`UserProofs/\` and whose contents are Lean source files only. A single-file project can be as small as \`UserProofs/Main.lean\`.

#### What is the difference between `fast` and `full` verification?

- Page URL: https://www.agentpmt.com/faq#faq-69cefe5cb1446c1c6d60b520
- Markdown URL: https://www.agentpmt.com/faq?format=agent-md#faq-69cefe5cb1446c1c6d60b520
- Tags: Product Specific

\`fast\` checks certificate details and hashes without rebuilding. \`full\` rebuilds and re-exports under the pinned runtime, then compares the regenerated output with the stored artifact for stronger assurance.

#### What should I save after a successful generation?

- Page URL: https://www.agentpmt.com/faq#faq-69cefe5bb1446c1c6d60b51f
- Markdown URL: https://www.agentpmt.com/faq?format=agent-md#faq-69cefe5bb1446c1c6d60b51f
- Tags: Product Specific

Save the generated output file, the certificate, the generation log, and especially \`artifacts.bundle.file\_id\`. The bundle is what you need for later verification.

#### Which target should I choose?

- Page URL: https://www.agentpmt.com/faq#faq-69cefe5bb1446c1c6d60b51e
- Markdown URL: https://www.agentpmt.com/faq?format=agent-md#faq-69cefe5bb1446c1c6d60b51e
- Tags: Product Specific

Use \`c\` when you want the broadest and lowest-risk support. Use \`rust\` when you want the same export path with Rust output. Use \`wasm\` only when you are comfortable with the current target being more constrained than \`c\`.

### Dependencies

This product has no public dependency products.