quantum-circuit-builder-with-proof

Quantum Circuit Builder with Proof: Use this product when a quantum circuit needs verifiable evidence, not just. Use when an agent needs quantum circuit builder with proof, 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, certify circuit, circuit, claims through AgentPMT-hosted remote tool calls.

Freshness

Last updated: 2026-09-07.

If the current date is more than 7 days after the last updated date, reinstall this skill from skills.sh or ClawHub before relying on endpoints, schemas, setup steps, or examples.

What This Tool Does

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.

Product Instructions

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:

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

Build and certify:

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

Receive external evidence:

1. Put the qpcert in File Manager.
2. Use verify_certificate with the independently supplied circuit and claims.
3. 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.

json

{"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.

json

{"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.

json

{"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.

json

{"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.

json

{"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.

json

{"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.

json

{"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.

json

{"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:

json

{
  "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.

json

{"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.

json

{"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.

json

{"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.

json

{"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.

json

{"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.

json

{"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.

json

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

When To Use

• Use this skill for Quantum Circuit Builder with Proof on AgentPMT.
• Use it when an agent needs this specific tool's behavior, schema, inputs, outputs, and invocation shape.
• Search and activation keywords: quantum circuit builder with proof, 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, certify circuit, circuit, claims.
• Supported action names: certify_circuit, certify_from_lean, execute_locally, export_provider_programs, extract_circuit, get_corpus_example, get_document, get_task, import_provider_circuit, inspect_circuit, instantiate_template, search_corpus_examples, search_knowledge, search_lean, verify_certificate.

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

Related Product Skills

• File Management: ../file-management (ClawHub: file-management, page: https://clawhub.ai/agentpmt/file-management; skills.sh: npx skills add AgentPMT/agent-skills --skill file-management)

Categories And Industries

No categories or industry tags are published for this tool.

Actions And Schema

Complete generated action schema: ./schema.md. Supported action count: 15. x402 availability: not enabled for this product.

• certify_circuit (action slug: certify-circuit): 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. Price: 10 credits. Parameters: circuit, claims.
• certify_from_lean (action slug: certify-from-lean): 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. Price: 15 credits. Parameters: claims, lean_source, resource_class.
• execute_locally (action slug: execute-locally): 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. Price: 15 credits. Parameters: lean_source, resource_class, shots.
• export_provider_programs (action slug: export-provider-programs): 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. Price: 10 credits. Parameters: export_targets, lean_source, resource_class.
• extract_circuit (action slug: extract-circuit): 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. Price: 10 credits. Parameters: certificate_file_id.
• get_corpus_example (action slug: get-corpus-example): 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. Price: 1 credits. Parameters: example_path.
• get_document (action slug: get-document): Use after search_knowledge to retrieve the complete selected knowledge record and provenance. Do not guess document IDs. Price: 1 credits. Parameters: document_id.
• get_task (action slug: get-task): 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. Price: 0 credits. Parameters: task_id.
• import_provider_circuit (action slug: import-provider-circuit): 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. Price: 3 credits. Parameters: circuit_id, provider_target, qubit_count, semantic_profile, source.
• inspect_circuit (action slug: inspect-circuit): 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. Price: 3 credits. Parameters: circuit, claims, image_format, include_visualizations.
• instantiate_template (action slug: instantiate-template): 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. Price: 2 credits. Parameters: descriptor.
• search_corpus_examples (action slug: search-corpus-examples): 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. Price: 1 credits. Parameters: query, result_count.
• search_knowledge (action slug: search-knowledge): 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. Price: 2 credits. Parameters: query, result_count, search_mode.
• search_lean (action slug: search-lean): 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. Price: 2 credits. Parameters: authoring_only, query, result_count.
• verify_certificate (action slug: verify-certificate): 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. Price: 10 credits. Parameters: certificate_file_id, circuit, claims.

Live Schema And Examples

Use the compact schema above for ordinary calls. Before a new production integration, or whenever parameters, enum values, nested objects, outputs, or examples are unclear, fetch live details first.

• Exact schema: call agentpmt-tool-search-and-execution with action: "get_schema", and tool_id: "quantum-circuit-builder-with-proof".
• Detailed examples: call agentpmt-tool-search-and-execution with action: "get_instructions" and tool_id: "quantum-circuit-builder-with-proof", or call this product with action: "get_instructions" when the product tool is already selected.
• Treat returned live schema and instructions as more specific than this generated summary.

MCP schema lookup through the main AgentPMT MCP server:

json

{
  "method": "tools/call",
  "params": {
    "name": "AgentPMT-Tool-Search-and-Execution",
    "arguments": {
      "action": "get_schema",
      "tool_id": "quantum-circuit-builder-with-proof"
    }
  }
}

For live examples, keep the same MCP tool and use these arguments:

json

{
  "action": "get_instructions",
  "tool_id": "quantum-circuit-builder-with-proof"
}

Authenticated AgentPMT REST schema lookup body:

json

{
  "name": "agentpmt-tool-search-and-execution",
  "parameters": {
    "action": "get_schema",
    "tool_id": "quantum-circuit-builder-with-proof"
  }
}

Authenticated AgentPMT REST live examples body:

json

{
  "name": "agentpmt-tool-search-and-execution",
  "parameters": {
    "action": "get_instructions",
    "tool_id": "quantum-circuit-builder-with-proof"
  }
}

Call This Tool

Product slug: quantum-circuit-builder-with-proof

Marketplace page: https://www.agentpmt.com/marketplace/quantum-circuit-builder-with-proof

• AgentPMT account route: first use ../agentpmt-account-mcp-rest-api-setup to connect the main MCP server or REST API for an Agent Group where this tool is enabled.
• x402 route: not enabled for this product.
• AgentPMT overview: use ../what-is-agentpmt for marketplace, Agent Group, workflow, MCP, REST, and payment concepts.

If those setup skills are not installed beside this product skill, use the downloads below.

Core AgentPMT setup skills:

• What AgentPMT is: ../what-is-agentpmt
  • ClawHub page: https://clawhub.ai/agentpmt/what-is-agentpmt
  • OpenClaw install: openclaw skills install what-is-agentpmt
  • skills.sh install: npx skills add AgentPMT/agent-skills --skill what-is-agentpmt
• AgentPMT account MCP/REST setup: ../agentpmt-account-mcp-rest-api-setup
  • ClawHub page: https://clawhub.ai/agentpmt/agentpmt-account-mcp-rest-api-setup
  • OpenClaw install: openclaw skills install agentpmt-account-mcp-rest-api-setup
  • skills.sh install: npx skills add AgentPMT/agent-skills --skill agentpmt-account-mcp-rest-api-setup

skills.sh install script:

bash

npx skills add AgentPMT/agent-skills --skill what-is-agentpmt
npx skills add AgentPMT/agent-skills --skill agentpmt-account-mcp-rest-api-setup

MCP call shape after the main AgentPMT MCP server is connected:

json

{
  "method": "tools/call",
  "params": {
    "name": "Quantum-Circuit-Builder-with-Proof",
    "arguments": {
      "action": "certify_circuit",
      "circuit": {
        "circuit_id": "example circuit id",
        "classical_bits": [
          {
            "id": "example id"
          }
        ],
        "initial_state": "zero",
        "metadata": {
          "name": "example name",
          "scope": "example scope"
        },
        "operations": [
          {
            "kind": "gate",
            "op_id": "example op id"
          }
        ],
        "qubits": [
          {
            "id": "example id"
          }
        ],
        "schema": "heyting.quantum_circuit_ir.v1",
        "semantic_profile": "unsigned_binary_symplectic_clifford_v1"
      },
      "claims": {
        "circuit_subject_sha256": "example circuit subject sha256",
        "claims": [
          {
            "accepted_evidence_tiers": [
              "example accepted evidence tier"
            ],
            "claim_id": "example claim id",
            "description": "example description",
            "statement": {
              "claim_type": "example claim type",
              "relation": "example relation"
            }
          }
        ],
        "ledger_id": "example ledger id",
        "schema": "heyting.quantum_claim_evidence.v1",
        "semantic_profile": "unsigned_binary_symplectic_clifford_v1"
      }
    }
  }
}

Use the exact tool name returned by tools/list; the name above is the expected readable form.

Authenticated AgentPMT REST call body:

json

{
  "name": "quantum-circuit-builder-with-proof",
  "parameters": {
    "action": "certify_circuit",
    "circuit": {
      "circuit_id": "example circuit id",
      "classical_bits": [
        {
          "id": "example id"
        }
      ],
      "initial_state": "zero",
      "metadata": {
        "name": "example name",
        "scope": "example scope"
      },
      "operations": [
        {
          "kind": "gate",
          "op_id": "example op id"
        }
      ],
      "qubits": [
        {
          "id": "example id"
        }
      ],
      "schema": "heyting.quantum_circuit_ir.v1",
      "semantic_profile": "unsigned_binary_symplectic_clifford_v1"
    },
    "claims": {
      "circuit_subject_sha256": "example circuit subject sha256",
      "claims": [
        {
          "accepted_evidence_tiers": [
            "example accepted evidence tier"
          ],
          "claim_id": "example claim id",
          "description": "example description",
          "statement": {
            "claim_type": "example claim type",
            "relation": "example relation"
          }
        }
      ],
      "ledger_id": "example ledger id",
      "schema": "heyting.quantum_claim_evidence.v1",
      "semantic_profile": "unsigned_binary_symplectic_clifford_v1"
    }
  }
}

Use the setup skill for the account connection details before making REST calls.

Response Handling

• Treat the returned JSON as the source of truth for this tool call.
• If the response includes warnings or correction targets, apply them before retrying.
• If the response includes a passed or success-style boolean, use it as the workflow gate.
• If validation fails or the response shape is unclear, call get_schema or get_instructions before retrying.
• If certify_circuit fails, preserve the request parameters and retry only after fixing schema, auth, or payment errors.

Security

• Do not place account secrets, wallet private keys, mnemonics, signatures, or payment headers in prompts or logs.
• Keep tool inputs scoped to the minimum content needed for the task.
• Use the setup skills for credential handling; this product skill only defines product-specific behavior.

AgentPMT Reference

• What AgentPMT is: ../what-is-agentpmt (ClawHub: what-is-agentpmt, page: https://clawhub.ai/agentpmt/what-is-agentpmt; skills.sh: npx skills add AgentPMT/agent-skills --skill what-is-agentpmt)
• AgentPMT account MCP/REST setup: ../agentpmt-account-mcp-rest-api-setup (ClawHub: agentpmt-account-mcp-rest-api-setup, page: https://clawhub.ai/agentpmt/agentpmt-account-mcp-rest-api-setup; skills.sh: npx skills add AgentPMT/agent-skills --skill agentpmt-account-mcp-rest-api-setup)
• Marketplace product: https://www.agentpmt.com/marketplace/quantum-circuit-builder-with-proof
• AgentPMT main MCP server: https://api.agentpmt.com/mcp/
• AgentPMT REST invoke endpoint: https://api.agentpmt.com/products/purchase