# Lean Proof To Solidity Smart Contract Generator ## Links - Product page URL: https://www.agentpmt.com/marketplace/lean-proof-to-solidity-smart-contract-generator - Product markdown URL: https://www.agentpmt.com/marketplace/lean-proof-to-solidity-smart-contract-generator?format=agent-md - Product JSON URL: https://www.agentpmt.com/marketplace/lean-proof-to-solidity-smart-contract-generator?format=agent-json ## Overview - Product ID: 69cedcb488254122a76adfbc - Type: function - Unit type: request - Price: 0 credits - Categories: Blockchain & Web3, Developer Tools, Compliance & Audit, Testing & QA, Automation, Data Validation & Verification - Generated at: 2026-06-24T08:13:14.228Z ### Page Description 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. ### Agent Description 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. ## Details ### 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. ### Actions - `catalog`: Fetch the advanced Lean catalog. Returns only the allowable advanced templates and reusable advanced Lean snippets. - `validate_lean`: Validate advanced Lean Solidity IR source immediately and return structured diagnostics that explain what is wrong before you submit a generation job. - `generate_solidity`: Generate Solidity from advanced Lean Solidity IR source and return a background task id for the generation job. - `compile_abi_bytecode`: Compile Solidity source and return ABI plus deployable bytecode immediately. - `encode_call`: Encode a contract function call using one ABI item and return the calldata immediately for later simulation or execution. - `evm_simulation`: Run offline EVM simulation against compiled contract output and return the result immediately. - `get_task`: Fetch the current status and result payload for a previously submitted background generate_solidity task within the caller's budget scope. - `list_tasks`: List recent background generate_solidity tasks for the caller's active budget only. ### 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 ### 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 - 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 ` ```bash curl -X POST "https://api.agentpmt.com/products/purchase" \ -H "Content-Type: application/json" \ -H "Authorization: Bearer eW91ci1hcGkta2V5LWhlcmU6eW91ci1idWRnZXQta2V5LWhlcmU=" \ -d '{ "product_id": "69cedcb488254122a76adfbc", "parameters": { "action": "catalog" } }' ``` ### 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. ### Schema #### Parameters - Schema type: actions ```json { "actions": { "catalog": { "description": "Fetch the advanced Lean catalog. Returns only the allowable advanced templates and reusable advanced Lean snippets.", "price_per_unit": 0 }, "validate_lean": { "description": "Validate advanced Lean Solidity IR source immediately and return structured diagnostics that explain what is wrong before you submit a generation job.", "properties": { "leanSourceText": { "type": "string", "description": "Lean source text that defines an advanced Solidity IR contract.", "required": true }, "leanSourceExpr": { "type": "string", "description": "Lean expression naming the contract value to validate, such as a `SolContract` declaration.", "required": true } }, "price_per_unit": 0 }, "generate_solidity": { "description": "Generate Solidity from advanced Lean Solidity IR source and return a background task id for the generation job.", "properties": { "leanSourceText": { "type": "string", "description": "Lean source text that defines an advanced Solidity IR contract.", "required": true }, "leanSourceExpr": { "type": "string", "description": "Lean expression naming the contract value to emit, such as a `SolContract` declaration.", "required": true } }, "price_per_unit": 0 }, "compile_abi_bytecode": { "description": "Compile Solidity source and return ABI plus deployable bytecode immediately.", "properties": { "solidityText": { "type": "string", "description": "Primary Solidity source file contents.", "required": true }, "sourceName": { "type": "string", "description": "Filename to assign to the primary Solidity source.", "required": false }, "contractName": { "type": "string", "description": "Optional specific contract name to select from the compiled output.", "required": false }, "extraSources": { "type": "array", "description": "Additional Solidity source files required for compilation.", "required": false, "items": { "type": "object" } } }, "price_per_unit": 0 }, "encode_call": { "description": "Encode a contract function call using one ABI item and return the calldata immediately for later simulation or execution.", "properties": { "abiItem": { "type": "object", "description": "Single ABI item describing the function to encode.", "required": true }, "args": { "type": "array", "description": "Ordered function arguments.", "required": false, "items": { "type": "string" } }, "label": { "type": "string", "description": "Optional label for the encoded call.", "required": false }, "valueWei": { "type": "string", "description": "Optional call value in wei.", "required": false }, "expectRevert": { "type": "boolean", "description": "Whether the later EVM simulation should expect a revert for this call.", "required": false }, "expectReturnHex": { "type": "string", "description": "Exact hex return value expected from the call.", "required": false }, "expectReturnStartsWith": { "type": "string", "description": "Hex prefix expected from the call result.", "required": false }, "expectReturnU256": { "type": "string", "description": "Expected uint256 result encoded as a decimal string.", "required": false }, "expectReturnAddress": { "type": "string", "description": "Expected address result.", "required": false }, "fromAlias": { "type": "string", "description": "Optional sender alias for the simulator.", "required": false }, "fromPrivateKeyHex": { "type": "string", "description": "Optional explicit private key for the sender.", "required": false } }, "price_per_unit": 0 }, "evm_simulation": { "description": "Run offline EVM simulation against compiled contract output and return the result immediately.", "properties": { "compileOutput": { "type": "object", "description": "Compiler output produced by the compile_abi_bytecode action.", "required": true }, "calls": { "type": "array", "description": "Sequence of encoded simulation calls to execute.", "required": false, "items": { "type": "object" } } }, "price_per_unit": 0 }, "get_task": { "description": "Fetch the current status and result payload for a previously submitted background generate_solidity task within the caller's budget scope.", "properties": { "task_id": { "type": "string", "description": "Task identifier returned by a prior background action.", "required": true } }, "price_per_unit": 0 }, "list_tasks": { "description": "List recent background generate_solidity tasks for the caller's active budget only.", "properties": { "limit": { "type": "integer", "description": "Maximum number of tasks to return.", "required": false } }, "price_per_unit": 0 } } } ``` ### Usage Instructions Use this tool to work directly in the advanced Lean Solidity IR lane. Recommended flow: 1. `catalog` 2. `validate_lean` 3. `generate_solidity` 4. `get_task` until the generation task reaches `completed` 5. `compile_abi_bytecode` 6. `encode_call` 7. `evm_simulation` 8. `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: ```json { "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: ```json { "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: ```json { "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? - 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 ", "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 69cedcb488254122a76adfbc ("Lean Proof To Solidity Smart Contract Generator"). 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. ### Dependencies This product has no public dependency products.