Quantum Circuit Builder with Proof

Name: Quantum Circuit Builder with Proof
Brand: Apoth3osis
SKU: 6a7e5036b8c970a6773201b5
Price: 0.10 USD
Availability: InStock

Function

Available ActionsEach successful request consumes credits as outlined below.

search_knowledge^2crsearch_lean^2crget_document^1crsearch_corpus_examples^1crget_corpus_example^1crinstantiate_template^2crimport_provider_circuit^3crinspect_circuit^3crcertify_circuit^10crcertify_from_lean^15crverify_certificate^10crextract_circuit^10crexport_provider_programs^10crexecute_locally^15crget_task

Details

Build quantum circuits that ship with a machine-checked proof. Quantum Circuit Builder with Proof turns an algorithm template, a Qiskit, Cirq, or Braket snippet, or Lean source into a normalized circuit, draws it as a downloadable PNG or JPEG diagram, and verifies the claims you state with the Lean 4 proof kernel. The result is a qpcert: a proof certificate anyone can replay independently, without trusting the agent that produced it. Export checked OpenQASM 3, Qiskit, Cirq, and Braket programs, run local simulations, and keep audit receipts for every step. Use it when a circuit must be audited, shared, or relied on. Plain Qiskit is simpler for throwaway experiments.

Use Cases

Formally verified quantum circuit design, Proof-carrying quantum circuit certificates (qpcert), Independent verification of a quantum proof certificate from another party, Audit-ready quantum computing artifacts for research and compliance, Import Qiskit Cirq and Braket circuits without executing code, Export verified OpenQASM 3 Qiskit Cirq and Braket programs, Quantum circuit diagrams as downloadable PNG or JPEG, GHZ Bernstein-Vazirani teleportation Grover and QFT circuit templates, Lean 4 quantum circuit proofs and theorem search, Local quantum circuit simulation with explicit measurement accounting, Reproducible quantum circuit exchange between AI agents and systems, Quantum computing research with a searchable knowledge base and Lean corpus

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(15)

search_knowledge^2cr3 params(1 required)

Use when the agent needs conceptual, research, architecture, or repository context before acting. Do not call as a mandatory preflight. Returns ranked results with source provenance; use get_document for the selected full record.

queryrequiredstring

Natural-language question, concept, quotation fragment, or repository term to find. Maximum 4000 characters.

result_countinteger

Maximum ranked results. Defaults to 8.

Default: 8

Range: 1 - 50

search_modestring

hybrid combines semantic and keyword matching; semantic favors meaning; keyword favors exact terms. Defaults to hybrid.

Values:

hybridsemantickeyword

Default: hybrid

search_lean^2cr3 params(1 required)

Use after starting from a worked CircuitSpec corpus example when the agent needs a Lean declaration, theorem, namespace, signature, or authoring primitive. authoring_only restricts results to the four modules admitted by submitted specs; false browses the wider reference corpus.

queryrequiredstring

Lean concept, identifier, theorem name, namespace, or signature fragment. Maximum 4000 characters.

result_countinteger

Maximum ranked results. Defaults to 8.

Default: 8

Range: 1 - 50

authoring_onlyboolean

When true, prefilter declarations to CircuitSpec, Qasm3Subset, Edifice.ProductionPurePipeline, and Edifice.ProductionEffectfulPipeline before ranking. Use true when writing submitted Lean; false browses the full reference catalog.

get_document^1cr1 param(1 required)

Use after search_knowledge to retrieve the complete selected knowledge record and provenance. Do not guess document IDs.

document_idrequiredinteger

Positive document ID returned by search_knowledge.

Range: 1 - ...

search_corpus_examples^1cr2 params

Use to find worked proof chains, template inputs, provider-intake samples, or designer samples in the bundled corpus. With no query, returns a bounded index. Results contain exact relative paths accepted by get_corpus_example.

querystring

Optional space-separated terms matched case-insensitively against stable example IDs, kinds, and asset paths.

result_countinteger

Maximum matching summaries. Defaults to 8.

Default: 8

Range: 1 - 50

get_corpus_example^1cr1 param(1 required)

Use after search_corpus_examples to retrieve one exact Lean, circuit, claims, qpcert, template, provider-intake, or designer-sample asset. The path is corpus-relative; traversal and absolute paths reject.

example_pathrequiredstring

Exact relative asset path returned by search_corpus_examples, such as authored_specs/bell_spec.lean.

instantiate_template^2cr1 param(1 required)

Use to create a normalized circuit from a supported GHZ, Bernstein-Vazirani, teleportation, Grover, or QFT template. This expands a template but does not certify it; pass the resulting circuit and claims to certify_circuit when proof is required.

descriptorrequiredobject

Typed template choice. ghz requires qubits 2-4096; bernstein_vazirani requires a binary secret; teleportation has no extra field; grover requires qubits 2-4096 and marked_item less than 2^qubits; qft requires qubits 2-6.

Properties:

semantic_profile*(string)- Exact semantics for the expanded circuit; choose a profile compatible with the selected family.

family*(string)- Template family. Family-specific fields are validated strictly.

qubits(integer)- Required for ghz, grover, and qft. QFT is limited to 6; other applicable families allow up to 4096.

secret(string)- Required only for bernstein_vazirani; a nonempty bit string containing only 0 and 1.

marked_item(integer)- Required only for grover; little-endian basis index satisfying 0 <= marked_item < 2^qubits.

import_provider_circuit^3cr5 params(4 required)

Use to parse bounded hand-authored Qiskit, Cirq, or Braket Python into normalized circuit IR without executing the source. This is parsing and round-trip validation, not proof. Use certify_circuit afterward when certification is required.

circuit_idrequiredstring

Stable lowercase identifier for the imported circuit.

Pattern: ^[a-z][a-z0-9_]{0,63}$

semantic_profilerequiredstring

Explicit semantic profile; the parser never guesses it.

Values:

unsigned_binary_symplectic_clifford_v1signed_binary_symplectic_v2exact_clifford_t_v2exact_clifford_t_measurement_v1exact_cyclotomic_2k_v1exact_cyclotomic_24_v1

provider_targetrequiredstring

Grammar used to parse source. Provider source is never executed.

Values:

qiskit_pythoncirq_pythonbraket_python

sourcerequiredstring

UTF-8 hand-authored provider source ending in exactly one newline. Qiskit requires exactly `from qiskit import QuantumCircuit` followed by `circuit = QuantumCircuit(N)`; aliases such as qc reject. Maximum 262144 characters. Generated or dynamic Python is outside the bounded grammar.

qubit_countinteger

Required for braket_python because Circuit() does not encode idle-wire width. Optional for Qiskit and Cirq, which declare width.

Range: 1 - 4096

inspect_circuit^3cr4 params(1 required)

Use for structural/semantic validation and subject-address computation before certification, or when visual explanations are useful. Validation and visualization are not proof or hardware execution. Set image_format to store a logical wire-circuit PNG or JPEG in the current budget's File Manager for display with AgentPMT's image card.

circuitrequiredobject

Complete heyting.quantum_circuit_ir.v1 object, normally returned by instantiate_template, import_provider_circuit, certify_from_lean diagnostics, or extract_circuit.

Properties:

schema*(string)- Circuit artifact schema.

circuit_id*(string)- Stable circuit identifier.

semantic_profile*(string)- Exact semantics under which operations are interpreted.

qubits*(array)- Nonempty ordered qubit declarations.

classical_bits*(array)- Ordered classical-bit declarations; may be empty.

initial_state*(string)- Declared initial state; current certified flows use zero.

operations*(array)- Ordered operations. Gate rows use kind, op_id, gate, controls, targets, parameters; measurement rows use basis, qubit, classical_bit; reset rows use qubit.

metadata(object)- Optional descriptive metadata; it does not create proof claims.

claimsobject

Optional heyting.quantum_claim_evidence.v1 ledger used only to enrich applicable visualizations. It is not certified by this action.

Properties:

schema*(string)- Claim-ledger artifact schema.

ledger_id*(string)- Stable ledger ID.

semantic_profile*(string)- Profile matching the circuit.

circuit_subject_sha256*(string)- Expected canonical circuit subject digest.

claims*(array)- Nonempty claim obligations with claim_id, statement, accepted_evidence_tiers, and description.

include_visualizationsboolean

When true, return all applicable structured semantic visualization lenses after validation. Defaults to false. This is independent of image_format.

image_formatstring

Optional stored image output. Set to png or jpeg to render the digest-bound logical wire_circuit projection, save it in budget-scoped File Manager, and return image_file metadata. The image is explanatory, not proof or hardware execution.

Values:

pngjpeg

certify_circuit^10cr2 params(2 required)

Use when a normalized circuit and an exact claim ledger are ready for kernel-backed certificate construction. The service validates the circuit, constructs the qpcert, and verifies its generated certificate; do not automatically call verify_certificate or extract_circuit on the fresh result.

circuitrequiredobject

Complete validated heyting.quantum_circuit_ir.v1 object. Required fields are schema, circuit_id, semantic_profile, nonempty qubits, classical_bits, initial_state, operations, and optional metadata; use inspect_circuit or a corpus .qcir.json example for the exact shape.

Properties:

schema*(string)- Circuit artifact schema.

circuit_id*(string)- Stable circuit identifier.

semantic_profile*(string)- Exact circuit semantics.

qubits*(array)- Nonempty qubit declarations.

classical_bits*(array)- Classical-bit declarations; may be empty.

initial_state*(string)- Initial state.

operations*(array)- Ordered gate, measure, and reset operations in canonical circuit IR form.

metadata(object)- Optional descriptive metadata.

claimsrequiredobject

Complete heyting.quantum_claim_evidence.v1 ledger bound to circuit_subject_sha256. Use a matching corpus .claims.json example; certification rejects unsupported or unbound claims.

Properties:

schema*(string)- Claim-ledger artifact schema.

ledger_id*(string)- Stable ledger ID.

semantic_profile*(string)- Must match circuit.semantic_profile.

circuit_subject_sha256*(string)- Canonical subject digest returned by inspection/import/template work.

claims*(array)- Nonempty exact claim obligations.

certify_from_lean^15cr3 params(1 required)

Use when restricted, internally trusted Lean CircuitSpec source is authoritative. Cloud Run executes Lean as trusted_direct_v1 in the shared service container; IAM authentication is not untrusted-code isolation. On success, returns a verified qpcert in File Manager; receipts report execution_mode and untrusted_code_isolation.

lean_sourcerequiredstring

Complete CircuitSpec authoring fragment defining spec. Use search_lean with authoring_only=true and a worked .lean corpus example when authoring. Maximum 1048576 characters.

resource_classstring

small supports up to 2 qubits; standard supports up to 4. The private runtime enforces a 300-second Lean budget.

Values:

smallstandard

claimsobject

Optional complete heyting.quantum_claim_evidence.v1 ledger. Omit to request the service's minimal well-formed claim; provide only when exact additional claims are required.

Properties:

schema*(string)- Claim-ledger artifact schema.

ledger_id*(string)- Stable ledger ID.

semantic_profile*(string)- Must match the emitted circuit.

circuit_subject_sha256*(string)- Canonical circuit subject digest.

claims*(array)- Nonempty exact claim obligations.

verify_certificate^10cr3 params(3 required)

Use at a trust boundary to independently replay a qpcert received from another party against separately supplied circuit and claims. Do not automatically re-verify a qpcert just produced by certify_circuit or certify_from_lean, because those actions already verify their generated certificate.

certificate_file_idrequiredstring

Budget-visible File Manager ID containing an application/vnd.heyting.qpcert+json certificate. Upload an external qpcert to File Manager first.

circuitrequiredobject

Complete independently supplied heyting.quantum_circuit_ir.v1 object expected to be bound by the certificate.

Properties:

schema*(string)- Circuit artifact schema.

circuit_id*(string)- Stable circuit ID.

semantic_profile*(string)- Exact circuit semantics.

qubits*(array)- Nonempty qubit declarations.

operations*(array)- Ordered canonical operations.

claimsrequiredobject

Complete independently supplied heyting.quantum_claim_evidence.v1 ledger expected to be bound by the certificate.

Properties:

schema*(string)- Claim-ledger artifact schema.

ledger_id*(string)- Stable ledger ID.

semantic_profile*(string)- Must match the circuit and certificate.

circuit_subject_sha256*(string)- Expected circuit subject digest.

claims*(array)- Exact claims expected to be certified.

extract_circuit^10cr1 param(1 required)

Use after receiving an existing qpcert when the normalized circuit and projections must be recovered by proof replay. Do not call merely to inspect a certificate just produced in the same flow.

certificate_file_idrequiredstring

Budget-visible File Manager ID containing a typed qpcert. The kernel replays the evidence before returning the normalized circuit.

export_provider_programs^10cr3 params(2 required)

Use to generate checked offline provider observation programs from internally trusted Lean. Lean runs as trusted_direct_v1 in the shared Cloud Run service container, not an untrusted-code sandbox. With no classical bits, .auto selects terminal_z_all and provider output materializes or records terminal measurement; compact results expose observation and measurement_injected. Output is not hardware execution or proof.

lean_sourcerequiredstring

Complete CircuitSpec authoring fragment defining spec. The current service export contract is Lean-owned; this action does not accept a qpcert.

export_targetsrequiredarray

One to four unique offline output targets. Current provider target snapshots are resolved privately by the connector.

Array of: string

resource_classstring

small supports up to 2 qubits; standard supports up to 4. Omit only when the service default is appropriate.

Values:

smallstandard

execute_locally^15cr3 params(2 required)

Use for local simulator observations from internally trusted Lean-owned construction, routing, and lowering. Lean runs as trusted_direct_v1 in the shared Cloud Run service container, not an untrusted-code sandbox. With no classical bits, .auto selects terminal_z_all; compact results expose observation and measurement_injected. Simulation is never a proof tier or hardware execution.

lean_sourcerequiredstring

Complete admitted Lean source defining spec with a LeanCPExecutableSpec instance.

shotsrequiredinteger

Number of local simulator shots.

Range: 1 - 65536

resource_classstring

small supports up to 2 qubits; standard supports up to 4.

Values:

smallstandard

get_task1 param(1 required)

Free polling action for one known background task. While processing, progress remains 0 because Lean exposes no trustworthy percentage; a moving date_updated and stage such as waiting_on_kernel show worker liveness. Poll with bounded backoff until completed or failed; outputs may contain File Manager references.

task_idrequiredstring

Exact budget-scoped UUID returned by the initiating action. Task IDs from another budget are not visible.

Pattern: ^[0-9a-fA-F-]{36}$

curl -X POST "https://api.agentpmt.com/products/purchase" \
  -H "Content-Type: application/json" \
  -H "Authorization: Bearer ********" \
  -d '{
    "product_id": "6a7e5036b8c970a6773201b5",
    "parameters": {
      "action": "search_knowledge",
      "query": "example_query",
      "result_count": 8,
      "search_mode": "hybrid"
    }
  }'

import requests
import json

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

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

data = {
    "product_id": "6a7e5036b8c970a6773201b5",
    "parameters": {
        "action": "search_knowledge",
        "query": "example_query",
        "result_count": 8,
        "search_mode": "hybrid"
    }
}

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: "6a7e5036b8c970a6773201b5",
  parameters: {
    "action": "search_knowledge",
    "query": "example_query",
    "result_count": 8,
    "search_mode": "hybrid"
  }
};

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: "6a7e5036b8c970a6773201b5",
  parameters: {
    "action": "search_knowledge",
    "query": "example_query",
    "result_count": 8,
    "search_mode": "hybrid"
  }
};

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.

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.

Recommended

Credit-Based Access Using AgentAddress

AgentAddress is preferred when an autonomous agent needs persistent file access, stored platform state, or maximum tool use ability across repeated calls.

Open Credit-Based Access Using AgentAddress

Direct x402 Payment

Use direct x402 for independent one-off tool calls that do not require shared files or stored platform state.

Accepted public payments

Stablecoin: USDC
Chains: Base, Arbitrum, Optimism, Polygon, and Avalanche

Direct x402 payments are not enabled for this product; use AgentAddress credit access instead.

Product Skill Package

This product has a published Agent Skill package. Install it when an autonomous agent needs product-specific operating instructions in its local skill registry.

Download SKILL.md View package source OpenClaw listing

OpenClaw install

skills.sh install

Usage Instructions

Usage guidance provided directly by the developer for this product.

Proof-Carrying Quantum

Use this product to research proof-carrying quantum concepts, find Lean declarations and worked corpus assets, build normalized circuits, create or independently verify kernel-backed qpcerts, export offline provider programs, and obtain local simulator observations.

The listed action schemas are the complete agent contract. Choose the action that advances the user's goal; there is no discovery preflight.

Trust boundaries

Knowledge and corpus results are reference material, not proof.
Provider-source import parses bounded source and never executes it. Parsing and round-trip validation are not proof.
Circuit inspection validates structure and semantics and can produce visual explanations, including a File Manager PNG or JPEG of the logical wire circuit. Validation and visualization are not proof or hardware execution.
certify_circuit and certify_from_lean create qpcerts through the pinned Lean kernel and verify the generated certificate before returning it.
verify_certificate is an independent recipient-side replay for evidence received from another party. Do not automatically verify a qpcert just produced by a certification action.
extract_circuit replays an existing qpcert before recovering its normalized circuit. It is optional, not a mandatory post-certification step.
Provider exports are offline source artifacts and receipts; they do not claim provider execution.
execute_locally returns simulator observations and receipts. Simulation does not add a proof tier.
Lean submitted to certify_from_lean, export_provider_programs, or execute_locally runs as trusted_direct_v1 inside the private Cloud Run service container. IAM authenticates callers, but Lean shares the service filesystem, network, and service identity; this is not untrusted-code isolation. Submit only internally trusted Lean. The receipt fields execution_mode and untrusted_code_isolation are the machine-readable authority.

Choose a flow

Research only when information is missing:

Use search_knowledge for concepts, design rationale, and repository documentation.
Use search_lean for declarations and authoring primitives; set authoring_only to true when writing submitted CircuitSpec source.
Use search_corpus_examples, then retrieve a selected asset with get_corpus_example.

Build and certify:

Start with instantiate_template, import_provider_circuit, or Lean source.
Use inspect_circuit when validation details or visualizations are useful.
Use certify_circuit for a normalized circuit plus an exact claim ledger, or certify_from_lean when Lean source is authoritative.
Optionally use export_provider_programs or execute_locally with Lean source.

Receive external evidence:

Put the qpcert in File Manager.
Use verify_certificate with the independently supplied circuit and claims.
Use extract_circuit only when the circuit must be recovered from the qpcert.

Choose the proof claim

Choose the narrowest claim that matches what the user actually asked to establish. If the user asks to "make a proof," "prove this circuit," or "create a certificate" without naming a stronger semantic property, default to a well-formed certificate. Never choose exactUnitary merely because the request uses the word "proof."

Well formed (well_formed in a claim ledger; .wellFormed in Lean) is the default for an arbitrary circuit built on the canvas, imported from a provider, or supplied as normalized IR. It proves that the circuit has nonzero width, has operations, and is admitted by the selected circuit/profile contract. It does not prove an algorithm result, a target state, or equivalence to a particular unitary. For certify_circuit, use inspect_circuit first when the canonical subject digest is not already available, then create a complete well-formed claim ledger bound to that digest. For certify_from_lean, use claims := [] and omit the request-level claims when only the service's minimal well-formed certificate is needed.
Exact unitary (.exactUnitary) is for a gate-only circuit when the user explicitly asks for its exact unitary semantics or an exact unitary equivalence. It rejects measurement and reset. Use it only with a matching checked-in corpus example, contracted template, or already-authored theorem and proof strategy. Exact matrix normalization can exhaust Lean heartbeats even for a short circuit; gate count alone is not a cost estimate.
Exact instrument (.exactInstrument) is for circuits with measurement or reset when the user explicitly asks to prove the exact measurement-channel/instrument semantics. Use a matching measurement/reset corpus example and its proof strategy; do not substitute it for ordinary structural certification.
Signed transport (.signedTransport) is for an explicitly requested Clifford signed-tableau/Pauli transport claim. Use it only when the circuit is supported by the Clifford translation and a matching corpus example or authored theorem exists.
Custom (.custom claimId statement) is for a specific trusted Lean proposition the user supplied or explicitly requested. It requires an authored proof of that exact proposition. Never invent a custom proposition and present it as the user's requested result.

Choose the certification action separately from the claim strength:

Use certify_circuit when the normalized circuit is authoritative. Prefer a matching certification_inputs result or .claims.json corpus asset. Do not translate a canvas circuit back into Lean merely to certify it.
Use certify_from_lean only when trusted Lean CircuitSpec source is itself authoritative or an exact/custom claim needs a matching Lean proof that is already supported by the corpus or supplied proof material.

If an exact semantic proof exhausts Lean heartbeats or another kernel resource limit, do not blindly increase maxHeartbeats, repeatedly submit the same expensive proof, or silently claim that a weaker certificate proves the exact property. If the original request was only for a generic certificate, start a new well-formed certification instead and describe its narrower scope. If the user explicitly requested the exact property, report that it was not proved and use a matching corpus theorem/proof strategy or ask before reducing the claim. PCQ_SERVICE_WARMING means no proof task started; retry the same chosen action after the service becomes ready.

Background tasks and files

Certification, certificate replay, extraction, provider export, and execution start persisted background tasks. The initiating action returns status: processing and a task_id immediately. Proof certification commonly takes 3-5 minutes, and larger or more complex proofs can take longer. Call the free get_task action with that ID using bounded backoff, normally every 3-10 seconds, until status is completed or failed. While processing, progress remains 0 because the Lean kernel does not report a trustworthy percentage. A changing date_updated and stage: waiting_on_kernel mean the worker is alive; continue polling and do not submit a duplicate paid proof task. Stages then move through packaging_result to completed.

On completion, the original action response is in outputs[0]. Results larger than 32 KiB are stored intact in File Manager as outputs[0].result_file; read that JSON file when needed. Certification always stores the full qpcert as outputs[0].certificate_file, even when the rest of the receipt is also moved to a result file. Files and tasks are budget-scoped.

On failure, read error and error_details. Correct invalid source, circuit, claims, or file input and start a new task. A retryable service failure says so explicitly; retry the same action later instead of running diagnostic actions.

Knowledge and corpus actions

`search_knowledge`

Use when conceptual or repository context is needed. Required: query. Optional: result_count 1-50, default 8; search_mode is hybrid, semantic, or keyword, default hybrid. Use get_document with a returned document ID when the full record is needed.

{"action":"search_knowledge","query":"why certificate replay is a trust boundary","result_count":6,"search_mode":"hybrid"}

`search_lean`

Use to find Lean declarations, theorem names, namespaces, signatures, and allowed authoring primitives. Required: query. Optional: result_count 1-50; authoring_only, default false. When writing a CircuitSpec, start with get_corpus_example for authored_specs/bell_spec.lean, then use authoring_only: true to look up names in the four admitted modules: CircuitSpec, Qasm3Subset, Edifice.ProductionPurePipeline, and Edifice.ProductionEffectfulPipeline. Use authoring_only: false to browse the wider reference corpus.

{"action":"search_lean","query":"CircuitSpec controlled X gate","result_count":8,"authoring_only":true}

`get_document`

Use after knowledge search. Required: positive document_id returned by search_knowledge. Do not guess IDs.

{"action":"get_document","document_id":42}

`search_corpus_examples`

Use to find worked proof chains, template inputs, provider-intake samples, or designer samples. Optional: query; omit it for a bounded index. Optional: result_count 1-50, default 8. Returned summaries contain exact asset paths.

{"action":"search_corpus_examples","query":"bell claims","result_count":10}

`get_corpus_example`

Use after corpus search. Required: the exact relative example_path. Absolute paths and traversal reject. JSON, Lean, qpcert, and text assets retain their media type; large assets may return a File Manager result file.

{"action":"get_corpus_example","example_path":"authored_specs/bell_spec.lean"}

Circuit actions

`instantiate_template`

Use to expand a supported template. Required: descriptor.semantic_profile and descriptor.family, plus family-specific fields:

ghz: qubits 2-4096.
bernstein_vazirani: nonempty binary secret.
teleportation: no additional field.
grover: qubits 2-4096 and marked_item satisfying 0 <= marked_item < 2^qubits.
qft: qubits 2-6.

The result is not certified. It normally includes the normalized circuit, validation/visualization material, and certification inputs where the template has contracted claims.

{"action":"instantiate_template","descriptor":{"semantic_profile":"exact_clifford_t_v2","family":"grover","qubits":3,"marked_item":5}}

`import_provider_circuit`

Use to parse hand-authored Qiskit, Cirq, or Braket Python without executing it. Required: circuit_id, explicit semantic_profile, provider_target, and source. The source must end in exactly one newline and is limited to 262144 characters. qubit_count is required for Braket because idle-wire width is not encoded by Circuit(); it is optional for Qiskit and Cirq.

Supported source targets are qiskit_python, cirq_python, and braket_python. The parser accepts only its bounded grammar; dynamic Python and arbitrary execution reject.

{"action":"import_provider_circuit","circuit_id":"bell_import","semantic_profile":"unsigned_binary_symplectic_clifford_v1","provider_target":"qiskit_python","source":"from qiskit import QuantumCircuit\ncircuit = QuantumCircuit(2)\ncircuit.h(0)\ncircuit.cx(0, 1)\n"}

`inspect_circuit`

Use for validation, canonical subject-address computation, and optional visual explanation. Required: complete circuit. Optional: claims to enrich claim-aware visualizations; include_visualizations, default false, to return the complete structured visualization pack; image_format (png or jpeg) to render the digest-bound logical wire_circuit projection and store it in the current budget's File Manager. image_format triggers the needed visualization internally and does not require include_visualizations: true.

The circuit must be a complete heyting.quantum_circuit_ir.v1 object with circuit_id, a supported semantic_profile, nonempty qubits, classical_bits, initial_state, and ordered operations. Gate rows use kind, op_id, gate, controls, targets, and parameters; measurement rows use basis, qubit, and classical_bit; reset rows use qubit.

When image_format is set, the response includes top-level image_file metadata. If a visual response is useful, immediately call AgentPMT's built-in present_resource_card with variant: "image" and image_file.file_id, filename, content_type, and size_bytes. Use file_id as the card's only locator: do not also pass url, and do not present or persist signed_url. The card resolves a fresh budget-scoped URL when it enters view or is replayed. The image is a logical explanation bound to the circuit and visualization digests; the qpcert, not the image, is the proof artifact.

{"action":"inspect_circuit","image_format":"png","circuit":{"schema":"heyting.quantum_circuit_ir.v1","circuit_id":"bell_pair","semantic_profile":"unsigned_binary_symplectic_clifford_v1","qubits":[{"id":"q0"},{"id":"q1"}],"classical_bits":[],"initial_state":"zero","operations":[{"kind":"gate","op_id":"g0","gate":"h","controls":[],"targets":["q0"],"parameters":[]},{"kind":"gate","op_id":"g1","gate":"cx","controls":["q0"],"targets":["q1"],"parameters":[]}],"metadata":{"name":"Bell pair","scope":"unsigned symplectic action"}}}

Then display the returned file with the chat card:

{
  "variant": "image",
  "title": "Bell pair logical circuit",
  "description": "Logical gate visualization; this image is not proof.",
  "file_id": "<image_file.file_id>",
  "filename": "<image_file.filename>",
  "content_type": "image/png",
  "size_bytes": 48321
}

Proof actions

`certify_circuit`

Use when a normalized circuit and exact claim ledger are ready. This is the normal path for a circuit built on the canvas, imported from a provider, or returned by a template. Required: complete circuit and claims. The claim ledger must use heyting.quantum_claim_evidence.v1, match the circuit's semantic profile and canonical subject digest, and contain nonempty typed claim obligations. Unless the user explicitly requested a supported stronger property, use a well_formed obligation. Start from matching certification_inputs or a .claims.json corpus example rather than inventing a relation or evidence tier.

This action validates the circuit, runs kernel-backed bundle construction, verifies the generated qpcert, stores it in File Manager, and returns a compact certificate summary. Do not automatically call verification or extraction on this fresh result.

{"action":"certify_circuit","circuit":{"schema":"heyting.quantum_circuit_ir.v1","circuit_id":"bell_pair","semantic_profile":"unsigned_binary_symplectic_clifford_v1","qubits":[{"id":"q0"},{"id":"q1"}],"classical_bits":[],"initial_state":"zero","operations":[{"kind":"gate","op_id":"g0","gate":"h","controls":[],"targets":["q0"],"parameters":[]},{"kind":"gate","op_id":"g1","gate":"cx","controls":["q0"],"targets":["q1"],"parameters":[]}],"metadata":{}},"claims":{"schema":"heyting.quantum_claim_evidence.v1","ledger_id":"bell_claims","semantic_profile":"unsigned_binary_symplectic_clifford_v1","circuit_subject_sha256":"c2324b23b67cc6eb4ce677e2b6f165c9000b6c87775e93e03fe2f422cd2c8201","claims":[{"claim_id":"bell_well_formed","statement":{"claim_type":"well_formed","profile":"unsigned_binary_symplectic_clifford_v1"},"accepted_evidence_tiers":["kernel_certified","checker_verified"],"description":"The normalized circuit is well formed in the active semantic profile."}],"evidence":[],"metadata":{"state":"obligations_only"}}}

`certify_from_lean`

Use only when restricted Lean CircuitSpec source is authoritative or the requested exact/custom claim has a matching trusted Lean proof. Do not convert a normalized canvas circuit to Lean just to obtain an ordinary certificate; use certify_circuit with a well-formed ledger instead. Required: lean_source defining spec. Optional: resource_class (small up to 2 qubits or standard up to 4); optional complete claims. When request-level claims are omitted, the service synthesizes a minimal well-formed claim. On rejection, the failed task contains Lean/kernel diagnostics; on success, it stores the complete qpcert. Cloud Run executes this Lean in the shared service container as trusted_direct_v1; IAM authentication is not untrusted-code isolation, so submit only internally trusted Lean and inspect the receipt fields.

{"action":"certify_from_lean","resource_class":"small","lean_source":"import HeytingLean.Quantum.ProofCarrying.CircuitSpec\n\nopen HeytingLean.Quantum.ProofCarrying\n\ndef spec : CircuitSpec where\n  circuitId := \"agent_bell\"\n  semanticProfile := \"unsigned_binary_symplectic_clifford_v1\"\n  qubits := 2\n  classicalBits := 0\n  ops := [.gate .H 0 0, .gate .CX 0 1]\n  claims := []\n  metadataScope := \"agent request\"\n\ntheorem spec_claims : CircuitSpec.ClaimsHold spec := by\n  simp [CircuitSpec.ClaimsHold, spec]\n"}

`verify_certificate`

Use to independently replay external evidence. Required: certificate_file_id, complete independently supplied circuit, and complete independently supplied claims. The file must contain a typed qpcert and be visible to the current budget. A mismatch between any of the three inputs rejects.

{"action":"verify_certificate","certificate_file_id":"2f5c8b82-3383-4d56-9ef2-c59546099e45","circuit":{"schema":"heyting.quantum_circuit_ir.v1","circuit_id":"bell_pair","semantic_profile":"unsigned_binary_symplectic_clifford_v1","qubits":[{"id":"q0"},{"id":"q1"}],"classical_bits":[],"initial_state":"zero","operations":[{"kind":"gate","op_id":"g0","gate":"h","controls":[],"targets":["q0"],"parameters":[]},{"kind":"gate","op_id":"g1","gate":"cx","controls":["q0"],"targets":["q1"],"parameters":[]}],"metadata":{}},"claims":{"schema":"heyting.quantum_claim_evidence.v1","ledger_id":"bell_claims","semantic_profile":"unsigned_binary_symplectic_clifford_v1","circuit_subject_sha256":"c2324b23b67cc6eb4ce677e2b6f165c9000b6c87775e93e03fe2f422cd2c8201","claims":[{"claim_id":"bell_well_formed","statement":{"claim_type":"well_formed","profile":"unsigned_binary_symplectic_clifford_v1"},"accepted_evidence_tiers":["kernel_certified","checker_verified"],"description":"The circuit is well formed."}],"evidence":[],"metadata":{}}}

`extract_circuit`

Use when an existing qpcert must be replayed and reduced to its normalized circuit and projections. Required: budget-visible certificate_file_id. Do not call this merely to repeat a fresh certification flow.

{"action":"extract_circuit","certificate_file_id":"2f5c8b82-3383-4d56-9ef2-c59546099e45"}

Provider and execution actions

`export_provider_programs`

Use to produce checked offline provider programs from Lean source. Required: lean_source defining spec; unique export_targets, one to four of openqasm3, qiskit_python, cirq_python, and braket_python. Optional: resource_class (small or standard).

The connector verifies and emits the Lean source, derives the circuit width, resolves current provider target snapshots internally, and invokes the Lean-owned export. This action does not accept a qpcert and does not submit to hardware. Its Lean runs as trusted_direct_v1 in the shared Cloud Run service container, not an untrusted-code sandbox.

When classicalBits := 0, Lean's default .auto observation is terminal_z_all. Provider outputs are runnable observation programs, so OpenQASM, Qiskit, and Cirq materialize terminal Z measurements and Braket records the equivalent terminal observation as implicit. The source circuit operations remain unchanged. Compact results report observation, source_operation_count, and measurement_injected so this materialization is explicit.

{"action":"export_provider_programs","resource_class":"small","export_targets":["openqasm3","qiskit_python"],"lean_source":"import HeytingLean.Quantum.ProofCarrying.CircuitSpec\n\nopen HeytingLean.Quantum.ProofCarrying\n\ndef spec : CircuitSpec where\n  circuitId := \"agent_bell\"\n  semanticProfile := \"unsigned_binary_symplectic_clifford_v1\"\n  qubits := 2\n  classicalBits := 0\n  ops := [.gate .H 0 0, .gate .CX 0 1]\n  claims := []\n  metadataScope := \"agent request\"\n\ntheorem spec_claims : CircuitSpec.ClaimsHold spec := by\n  simp [CircuitSpec.ClaimsHold, spec]\n"}

`execute_locally`

Use for local simulator observations from Lean-owned construction, routing, and lowering. Required: lean_source defining spec with a LeanCPExecutableSpec instance; shots 1-65536. Optional: resource_class (small or standard). The service chooses a compatible bundled backend; there is no backend-selection field. With classicalBits := 0, .auto observes terminal Z on every qubit, which makes the simulation runnable without adding measure operations to the authored spec. Compact results report that observation and whether measurements were injected. Lean runs as trusted_direct_v1 in the shared Cloud Run service container, not an untrusted-code sandbox.

{"action":"execute_locally","resource_class":"small","shots":1024,"lean_source":"import HeytingLean.Quantum.ProofCarrying.CircuitSpec\n\nopen HeytingLean.Quantum.ProofCarrying\n\ndef spec : CircuitSpec where\n  circuitId := \"agent_bell\"\n  semanticProfile := \"unsigned_binary_symplectic_clifford_v1\"\n  qubits := 2\n  classicalBits := 0\n  ops := [.gate .H 0 0, .gate .CX 0 1]\n  claims := []\n  metadataScope := \"agent request\"\n\ntheorem spec_claims : CircuitSpec.ClaimsHold spec := by\n  simp [CircuitSpec.ClaimsHold, spec]\n"}

Task action

`get_task`

Use only with the exact task_id returned by a long-running action. This action costs zero credits. Poll with bounded backoff; do not create duplicate paid work while the original task is still processing. During Lean work, progress deliberately stays 0 rather than inventing a percentage; a moving date_updated heartbeat and the current stage show that the worker is alive.

{"action":"get_task","task_id":"12345678-1234-1234-1234-123456789012"}

About this Product

Quantum circuits with a proof you can check yourself

Any AI agent can write Qiskit. This tool is for the moments when generated code is not enough: the circuit will be reviewed by someone else, reused by another system, translated to a different quantum framework, or kept as an auditable record of exactly what was verified.

Quantum Circuit Builder with Proof normalizes your circuit, checks the claims you state with the Lean 4 proof kernel, and returns a qpcert, a proof certificate bound to that exact circuit and those exact claims. Anyone who receives the certificate can replay the proof on their own instead of taking the agent's word for it.

How it works

Start a circuit. Expand a built-in template (GHZ, Bernstein-Vazirani, teleportation, Grover, or QFT), paste hand-written Qiskit, Cirq, or Braket Python, or supply a Lean CircuitSpec. Provider code is parsed, never executed.
Inspect it. The circuit is validated against its semantic profile and given a content address (a SHA-256 digest of the normalized circuit). Optionally render the logical wire circuit as a PNG or JPEG that appears in chat and is saved to your File Manager.
Certify the claims. State what you want proved, most often that the circuit is well formed under its profile. The Lean kernel constructs and verifies the proof and returns the qpcert.
Share and verify. Hand the circuit, claim ledger, and qpcert to a colleague, reviewer, or another agent. They replay the certificate against their own copy of the inputs. Any mismatch is rejected.
Export or simulate. Generate OpenQASM 3, Qiskit, Cirq, or Braket programs that are read back and checked against the certified circuit, or run a local simulation with a clearly labeled observation.

What you get

Fail-closed intake: unsupported or ambiguous source is rejected instead of guessed or executed.
A proof certificate: a kernel-backed qpcert for the exact normalized circuit and the stated claims.
Independent replay: a recipient verifies received evidence against separately supplied circuit and claim inputs.
Translation integrity: exported programs are parsed back and checked, so drift between frameworks is surfaced.
Explicit measurement accounting: if a terminal measurement is added to make an export or simulation runnable, the receipt says so.
Circuit diagrams: a digest-bound PNG or JPEG of the logical wire circuit, shown inline and downloadable.
Audit receipts: inputs, verification results, execution mode, observation choices, and artifact references for every step.
Research tools: a searchable knowledge base, Lean declaration search, and a corpus of worked proof examples.

Supported inputs and outputs

Input	Output
Templates: GHZ (2 to 4096 qubits), Bernstein-Vazirani, teleportation, Grover (2 to 4096 qubits), QFT (2 to 6 qubits)	qpcert proof certificate (stored in File Manager)
Hand-written Qiskit, Cirq, or Braket Python (bounded grammar, never executed)	OpenQASM 3, Qiskit, Cirq, and Braket programs with readback receipts
Lean `CircuitSpec` source (up to 2 qubits small, up to 4 qubits standard)	PNG or JPEG circuit diagram bound to the circuit digest
Normalized circuit IR (`heyting.quantum_circuit_ir.v1`)	Local simulator observations and execution receipts
An existing qpcert from another party	Independent verification result, or the recovered normalized circuit

Gates: id h x y z s sdg t tdg cx cz swap, plus exact cyclotomic phase gates under the exact_cyclotomic_2k_v1 profile. Measurement, reset, and barrier operations are supported.

Who it is for

Quantum researchers who need a reproducible, verifiable artifact alongside a paper or dataset.
Engineering teams exchanging circuits between people, agents, or pipelines and translating them across frameworks.
Auditors and reviewers who must confirm a received circuit and certificate without trusting the sender.
Educators and students learning how formal verification applies to quantum circuits.

When plain Qiskit is the better choice

For a quick experiment, a tutorial, or a disposable Bell pair, have your agent write Qiskit directly. Use this tool when the circuit is consequential: it will be published, evaluated automatically, exchanged between parties, translated across providers, or relied on as a verified artifact.

What the proof does and does not mean

It proves only the claims explicitly encoded and accepted by the verifier, not every desirable property of the circuit.
Structural validation, circuit diagrams, provider-source parsing, and round-trip checks are not proof.
Simulation returns sampled observations. It is not a proof tier and says nothing about physical hardware fidelity.
Provider exports are offline programs. They are not evidence that a provider or quantum device executed them.
Submitted Lean runs as trusted_direct_v1 in the shared service container. Callers are authenticated, but this is not untrusted-code isolation. Submit only Lean you trust.

Cost and timing

Research and inspection actions cost 1 to 3 credits. Certification, verification, extraction, export, and simulation cost 10 to 15 credits each and run as background tasks. A typical proof completes in 3 to 5 minutes; polling the task is free.

Glossary

qpcert: a quantum proof certificate. A file that binds a normalized circuit, a claim ledger, and a Lean proof, and that can be replayed by anyone.
Claim ledger: the explicit list of properties to prove, each tied to the circuit's digest.
Well formed: the default claim. The circuit has qubits and operations and is admitted by its semantic profile. It does not claim a target state or algorithm result.
Semantic profile: the gate set and interpretation the circuit is checked under, such as exact Clifford+T or stabilizer.
Lean kernel: the pinned Lean 4 proof checker that constructs and replays every certificate.

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 6a7e5036b8c970a6773201b5 ("Quantum Circuit Builder with Proof"). 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 see a diagram of my circuit?

Yes. Ask for a PNG or JPEG when inspecting the circuit. The diagram shows the logical wire circuit, is bound to the circuit's digest, appears inline in chat, and is saved to your File Manager for download. The diagram is explanatory only; the qpcert is the proof.

Can I submit untrusted Lean code?

No. Submitted Lean runs inside the shared service container. Callers are authenticated, but the code is not isolated as untrusted, and the receipt reports this as execution mode trusted_direct_v1 with untrusted-code isolation false. Submit only Lean you or your organization trust.

Does a qpcert prove that every aspect of the circuit is correct?

No. A qpcert covers only the claims written in the claim ledger and accepted by the verifier. Parsing, structural validation, diagrams, round-trip checks, and simulation do not become proof just because they happen in the same workflow.

Does provider export prove that the circuit ran on quantum hardware?

No. Export produces offline programs and readback receipts, and local execution produces simulator observations. Neither shows that a provider ran the circuit or says anything about physical hardware fidelity.

How does someone else verify a certificate I send them?

They upload the qpcert to their File Manager and run verification with their own copy of the circuit and claims. The Lean kernel replays the proof and rejects any mismatch between the certificate and the supplied inputs, so they never have to trust you or the agent that produced it.

How long does certification take, and what does it cost?

Certification runs in the background and typically completes in 3 to 5 minutes; larger or exact semantic proofs can take longer. Certifying a circuit costs 10 credits, certifying from Lean 15, and verifying or extracting a received certificate 10. Checking on a task is free.

What does "well formed" mean, and is that the default proof?

Yes, it is the default. A well-formed certificate proves the circuit has at least one qubit and one operation and is admitted by its semantic profile. It does not prove an algorithm result, a target state, or equivalence to a specific unitary. Stronger claims such as exact unitary, exact instrument, or signed transport are available when you ask for them and a matching proof strategy exists.

What is a qpcert?

A qpcert is a quantum proof certificate. It is a file that binds three things together: the normalized circuit, the list of claims you asked to prove, and the Lean proof that those claims hold. Anyone who has the file can replay the proof themselves. It is the product's proof artifact; diagrams, receipts, and simulation results are not.

Which algorithm templates are included?

GHZ states (2 to 4096 qubits), Bernstein-Vazirani with any binary secret, quantum teleportation, one-iteration Grover search (2 to 4096 qubits), and the quantum Fourier transform (2 to 6 qubits). A template gives you a normalized circuit and certification inputs; certification is a separate step.

Which quantum frameworks and formats are supported?

Input: hand-written Qiskit, Cirq, or Braket Python, Lean CircuitSpec source, normalized circuit IR, or a built-in template. Output: OpenQASM 3, Qiskit, Cirq, and Braket programs, each parsed back and checked against the certified circuit before it is returned.

Why do exported programs contain measurements I did not write?

When a circuit declares no classical bits, the default observation is a terminal Z measurement on every qubit. Runnable exports and simulations add that measurement so the program can actually produce results. The receipt reports the observation, the original operation count, and whether measurement was injected, so nothing is hidden.

Why use this instead of asking an agent to write Qiskit directly?

For quick experiments, direct Qiskit is simpler and usually the better choice. Use this product when the result has to cross a trust boundary or be audited: it binds a normalized circuit and explicit claims to a proof certificate that a recipient can replay independently, and it checks exported programs for translation drift.

Quantum Circuit Builder with Proof

Available ActionsEach successful request consumes credits as outlined below.

Details

Use Cases

Dynamic MCP Setup

30 Second Setup

Hosted Streamable HTTPS

Config Example

About this Product

Quantum circuits with a proof you can check yourself

How it works

What you get

Supported inputs and outputs

Who it is for

When plain Qiskit is the better choice

What the proof does and does not mean

Cost and timing

Glossary

Frequently Asked Questions

How do I connect this tool to an external agent?

How does an external agent use this tool?

Can I see a diagram of my circuit?

Can I submit untrusted Lean code?

Does a qpcert prove that every aspect of the circuit is correct?

Does provider export prove that the circuit ran on quantum hardware?

How does someone else verify a certificate I send them?

How long does certification take, and what does it cost?

What does "well formed" mean, and is that the default proof?

What is a qpcert?

Which algorithm templates are included?

Which quantum frameworks and formats are supported?

Why do exported programs contain measurements I did not write?

Why use this instead of asking an agent to write Qiskit directly?

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