Lean Proof To Solidity Smart Contract Generator by Apoth3osis

Name: Lean Proof To Solidity Smart Contract Generator
Brand: Apoth3osis
SKU: 69cedcb488254122a76adfbc
Availability: InStock

Lean Proof To Solidity Smart Contract Generator

Function

Available ActionsEach successful request consumes credits as outlined below.

catalogvalidate_leangenerate_soliditycompile_abi_bytecodeencode_callevm_simulationget_tasklist_tasks

Details

PROOF OF CONCEPT - This tool does not include an exhaustive Lean to Solidity code mapping, but it shows the capabilities of our system and the value of going from proven Lean straight to Solidity. Build your logic in a proven language first, then generate your Solidity from that. We have included Lean templates and allowable Lean snippets to get you started. Try it live in the builder, or use the AI agent to help you build faster. The tool allows you to validate Lean, generate Solidity from it, compile the generated Solidity to ABI and bytecode, encode ABI calls, and then run offline EVM simulation before deployment. The full system is available for licensing - inquire directly if interested.

Use Cases

Fetch allowable advanced Lean templates and snippets, Validate advanced Lean Solidity IR before generation, Generate Solidity from advanced Lean Solidity IR, Compile generated Solidity to ABI and bytecode, Encode ABI function calls for simulation, Run offline EVM simulation before deployment, Poll background Lean generation tasks within the active budget

Dynamic MCP Setup

Connect once through AgentPMT Dynamic MCP, then use approved tools from the same agent connection.

30 Second Setup

STDIO connector for Claude Code, Codex, Cursor, Zed, and other LLMs that require STDIO or custom connections.

npm install -g @agentpmt/mcp-routeragentpmt-setup

Hosted Streamable HTTPS

MCP endpoint for browser-based apps like ChatGPT, Claude, Grok, or any time you want a streamable connection with no local install.

https://api.agentpmt.com/mcp

Config Example

Use the hosted endpoint directly in clients that support remote MCP. Store your Bearer token in the client config or secret field.

Full connection guide

{
  "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\"}"
      }
    }
  }
}

Need client videos, organization controls, audit details, and the full feature overview?

More About Dynamic MCP

Actions(8)

catalog0 params

Fetch the advanced Lean catalog. Returns only the allowable advanced templates and reusable advanced Lean snippets.

No parameters for this action.

validate_lean2 params(2 required)

Validate advanced Lean Solidity IR source immediately and return structured diagnostics that explain what is wrong before you submit a generation job.

leanSourceTextrequiredstring

Lean source text that defines an advanced Solidity IR contract.

leanSourceExprrequiredstring

Lean expression naming the contract value to validate, such as a `SolContract` declaration.

generate_solidity2 params(2 required)

Generate Solidity from advanced Lean Solidity IR source and return a background task id for the generation job.

leanSourceTextrequiredstring

Lean source text that defines an advanced Solidity IR contract.

leanSourceExprrequiredstring

Lean expression naming the contract value to emit, such as a `SolContract` declaration.

compile_abi_bytecode4 params(1 required)

Compile Solidity source and return ABI plus deployable bytecode immediately.

solidityTextrequiredstring

Primary Solidity source file contents.

sourceNamestring

Filename to assign to the primary Solidity source.

contractNamestring

Optional specific contract name to select from the compiled output.

extraSourcesarray

Additional Solidity source files required for compilation.

Array of: object

encode_call11 params(1 required)

Encode a contract function call using one ABI item and return the calldata immediately for later simulation or execution.

abiItemrequiredobject

Single ABI item describing the function to encode.

argsarray

Ordered function arguments.

Array of: string

labelstring

Optional label for the encoded call.

valueWeistring

Optional call value in wei.

expectRevertboolean

Whether the later EVM simulation should expect a revert for this call.

expectReturnHexstring

Exact hex return value expected from the call.

expectReturnStartsWithstring

Hex prefix expected from the call result.

expectReturnU256string

Expected uint256 result encoded as a decimal string.

expectReturnAddressstring

Expected address result.

fromAliasstring

Optional sender alias for the simulator.

fromPrivateKeyHexstring

Optional explicit private key for the sender.

evm_simulation2 params(1 required)

Run offline EVM simulation against compiled contract output and return the result immediately.

compileOutputrequiredobject

Compiler output produced by the compile_abi_bytecode action.

callsarray

Sequence of encoded simulation calls to execute.

Array of: object

get_task1 param(1 required)

Fetch the current status and result payload for a previously submitted background generate_solidity task within the caller's budget scope.

task_idrequiredstring

Task identifier returned by a prior background action.

list_tasks1 param

List recent background generate_solidity tasks for the caller's active budget only.

limitinteger

Maximum number of tasks to return.

curl -X POST "https://api.agentpmt.com/products/purchase" \
  -H "Content-Type: application/json" \
  -H "Authorization: Bearer ********" \
  -d '{
    "product_id": "69cedcb488254122a76adfbc",
    "parameters": {
      "action": "catalog"
    }
  }'

import requests
import json

url = "https://api.agentpmt.com/products/purchase"

headers = {
    "Content-Type": "application/json",
    "Authorization": "Bearer ********"
}

data = {
    "product_id": "69cedcb488254122a76adfbc",
    "parameters": {
        "action": "catalog"
    }
}

response = requests.post(url, headers=headers, json=data)
print(response.status_code)
print(response.json())

const url = "https://api.agentpmt.com/products/purchase";

const headers = {
  "Content-Type": "application/json",
  "Authorization": "Bearer ********"
};

const data = {
  product_id: "69cedcb488254122a76adfbc",
  parameters: {
    "action": "catalog"
  }
};

fetch(url, {
  method: "POST",
  headers,
  body: JSON.stringify(data)
})
  .then(response => response.json())
  .then(data => console.log(data))
  .catch(error => console.error("Error:", error));

const axios = require('axios');

const url = "https://api.agentpmt.com/products/purchase";

const headers = {
  "Content-Type": "application/json",
  "Authorization": "Bearer ********"
};

const data = {
  product_id: "69cedcb488254122a76adfbc",
  parameters: {
    "action": "catalog"
  }
};

axios.post(url, data, { headers })
  .then(response => {
    console.log(response.status);
    console.log(response.data);
  })
  .catch(error => {
    console.error("Error:", error.message);
  });

Login to view your API and budget keys. The example above uses placeholder values. Sign in to see personalized code with your bearer token.

Usage Instructions

Usage guidance provided directly by the developer for this product.

Use this tool to work directly in the advanced Lean Solidity IR lane.

Recommended flow:

catalog
validate_lean
generate_solidity
get_task until the generation task reaches completed
compile_abi_bytecode
encode_call
evm_simulation
list_tasks only when you need to review recent generation jobs in your current budget scope

Action breakdown

catalog

Purpose: Fetch the allowable advanced Lean templates and reusable advanced Lean snippets.
Output: immediate payload containing only advancedTemplates and advancedSnippets.

Example:

{
  "action": "catalog"
}

validate_lean

Purpose: Validate advanced Lean Solidity IR source before running a generation job.
Use it for: checking that the Lean source parses, resolves the target expression, and is suitable for the advanced Solidity generator.
Input: leanSourceText and leanSourceExpr.
Output: immediate validation result. On failure it returns a human summary, stable errorKind, and parsed diagnostics with submitted line and column information.

Example:

{
  "action": "validate_lean",
  "leanSourceText": "import HeytingLean.LeanSP.Emit.SolEmit\n\nnamespace Demo\nopen LeanSP.Emit\n\ndef counter : SolContract :=\n  { name := \"Counter\"\n  , stateVars := [ { name := \"storedValue\", ty := .uint 256, visibility := .pub } ]\n  , functions :=\n      [ { name := \"setValue\"\n        , params := [(\"newValue\", .uint 256)]\n        , visibility := .external\n        , body := [ .assign (.var \"storedValue\") (.var \"newValue\") ]\n        }\n      ]\n  }\n",
  "leanSourceExpr": "Demo.counter"
}

generate_solidity

Purpose: Generate Solidity from advanced Lean Solidity IR source.
Use it for: users who already understand the Lean authoring model and want Solidity out.
Input: leanSourceText and leanSourceExpr.
Output: a background task id. Poll with get_task until the task reaches completed. The completed result includes emitted Solidity text and related metadata.

Example:

{
  "action": "generate_solidity",
  "leanSourceText": "import HeytingLean.LeanSP.Emit.SolEmit\n\nnamespace Demo\nopen LeanSP.Emit\n\ndef counter : SolContract :=\n  { name := \"Counter\"\n  , stateVars := [ { name := \"storedValue\", ty := .uint 256, visibility := .pub } ]\n  , functions :=\n      [ { name := \"setValue\"\n        , params := [(\"newValue\", .uint 256)]\n        , visibility := .external\n        , body := [ .assign (.var \"storedValue\") (.var \"newValue\") ]\n        }\n      ]\n  }\n",
  "leanSourceExpr": "Demo.counter"
}

compile_abi_bytecode

Purpose: Compile Solidity and return ABI plus bytecode.
Use it for: turning generated Solidity text into deployable artifacts.
Input: solidityText and optionally sourceName, contractName, and extraSources.
Output: immediate compile payload with ABI, bytecode, deployed bytecode, and selected contract metadata.

encode_call

Purpose: Encode calldata for a function call using an ABI item.
Use it for: preparing calls for EVM simulation.

evm_simulation

Purpose: Run an offline EVM simulation against compiled contract output.
Use it for: checking generated contract behavior before deployment.

get_task

Purpose: Fetch the current status and result for a background task.
Use it for: polling generate_solidity.

list_tasks

Purpose: List your recent background tasks in the current budget scope.
Use it for: finding recent advanced Lean generation jobs without storing every task id yourself.

Notes:

catalog returns immediately with only the advanced templates and snippet catalog.
validate_lean returns immediately with structured diagnostics.
generate_solidity submits a background task.
compile_abi_bytecode, encode_call, and evm_simulation return immediately.
get_task and list_tasks are restricted to the caller's active budget scope.
The restricted builder and component-composition paths still exist in the backend, but they are intentionally hidden from the current user-facing product surface.

Frequently Asked Questions

How do I connect this tool to an external agent?

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

Install commands

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:

Hosted MCP config

{
  "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 for more details.

How does an external agent use this tool?

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

Agent prompt

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 69cedcb488254122a76adfbc ("Lean Proof To Solidity Smart Contract Generator"). After reading the schema and any returned instructions, tell me what this tool can do, what inputs it needs, and what you need from me before running it. Do not call action 'call_tool' until I confirm the request and provide the required parameters.

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

Lean Proof To Solidity Smart Contract Generator

Available ActionsEach successful request consumes credits as outlined below.

Details

Use Cases

Dynamic MCP Setup

30 Second Setup

Hosted Streamable HTTPS

Config Example

Actions(8)

Credit-Based Access Using AgentAddress

Direct x402 Payment

Usage Instructions

Frequently Asked Questions

How do I connect this tool to an external agent?

How does an external agent use this tool?

Lean To Solidity

Lean Snippets

Looking for help integrating AI into your business? Set up a free consultation.