# 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
- Vendor: Apoth3osis
- 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-05-21T01:24:58.518Z

### 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

No related content is currently linked to this product.

## Integration Details

### DynamicMCP

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

STDIO connector for Claude Code, Codex, Cursor, Zed, and other LLMs that require STDIO or custom connections. This lightweight connector routes requests to `https://api.agentpmt.com/mcp`. All tool execution happens in the cloud and the server cannot edit any files on your computer.

```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

Do not use the abbreviated instructions in this product markdown for wallet-based invocation. Retrieve the full External Agent API markdown document instead.

- External Agent API page URL: https://www.agentpmt.com/external-agent-api
- External Agent API markdown URL: https://www.agentpmt.com/external-agent-api?format=agent-md

### 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

#### 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.