WritersLogic Verifiable AI Agent Hub Prove Contract Logic API
The Prove Contract Logic API from WritersLogic Verifiable AI Agent Hub — 1 operation(s) for prove contract logic.
Work with this as data
Every API here is available over the APIs.io API and to AI agents over MCP.
MCP server
One button, every client — Claude, Cursor, VS Code and the rest.
https://apis.io/mcp
Tools for apis
7 MCP tools reach this
find_apisBrowse and filter every API in the catalog.get_api_artifactsOne API's artifacts, grouped by type.get_openapiThe primary OpenAPI for this API.find_similar_apisAPIs that look like this one.apis_io_searchSTART HERE — APIs, providers and tags for one query, each with its total.resolveTurn a domain, URL or GitHub org into the provider it belongs to.find_cohortsEvery scored population of providers in the catalog.
Call it yourself
curl for this page
This API
curl "https://apis.io/api/v1/apis/writerslogic-com:writerslogic-com-prove-contract-logic-api"
All apis
curl "https://apis.io/api/v1/apis?limit=25"Calls without X-API-Key need no key. Calls with it need a paid plan — get a key.
Get an API key
Free tier, no form to fill in. Signing in shares your email address with us — we store it to create your key and to recognise you if you sign in with another provider. See our Privacy Policy and Terms.
A second provider on the same verified email joins the account you already have.
OpenAPI Specification
openapi: 3.2.0
info:
title: WritersLogic Verifiable AI Agent Hub Prove Contract Logic…
version: 2.0.0
description: Pay-per-call agents settled in USDC on Base via x402. Every response carries a signed provenance envelope.
contact:
name: WritersLogic
url: https://writerslogic.com/agents
email: agents@writerslogic.com
servers:
- url: https://agents.writerslogic.com
tags:
- name: Prove Contract Logic
paths:
/api/v1/prove-contract-logic:
post:
operationId: smt_contract_prover
summary: SMT Contract & Policy Logic Prover
description: 'Answers a yes/no logic question about contract clauses, IAM/OPA policies or business rules with a solver-backed result and a plain-language headline and next step. Takes clauses or pasted text (or a formal IR directly with zero LLM calls), formalizes them into typed Boolean, integer and rational constraints, then answers "is P possible", "does invariant I always hold" or "are any clauses contradictory" with a pure-TypeScript CDCL(T) solver (exact rational simplex, branch-and-bound, minimal unsatisfiable cores). SAT returns an exact counterexample checked against every original constraint; UNSAT reports the proof statement and the minimal conflicting clause ids; exhausted budgets return UNKNOWN. Natural-language input uses two independent formalizations whose logical equivalence is checked by the solver; disagreements are reported with a distinguishing assignment and lower confidence. Formal elements whose source quote is not in the text are dropped. The proof is exact for the formalization, not for the original wording, and is not legal advice.
Price: 2.50 USDC on Base (x402).'
x-x402-price-usdc: '2.50'
x-x402-amount: '2500000'
x-payment-info:
protocols:
- x402
price:
mode: fixed
currency: USD
amount: '2.50'
x-audience: developer
x-sample-url: https://agents.writerslogic.com/api/v1/samples/smt-contract-prover
security:
- x402: []
- apiKey: []
requestBody:
required: true
content:
application/json:
schema:
type: object
additionalProperties: false
properties:
clauses:
type: array
minItems: 1
maxItems: 200
description: Natural-language contract clauses, IAM/OPA policy statements or business rules, each with a caller-chosen id. Mutually exclusive with ir.
items:
type: object
additionalProperties: false
required:
- id
- text
properties:
id:
type: string
minLength: 1
maxLength: 64
text:
type: string
minLength: 1
maxLength: 4000
text:
type: string
minLength: 3
maxLength: 60000
description: 'Alternative to clauses: the contract, policy or rules pasted as plain text. It is split into clauses by blank lines and numbered or bulleted lines (ids C1.2 or S3). Use clauses when you need your own ids. Requires query.'
query:
type: string
minLength: 1
maxLength: 1000
description: The question, e.g. "Can an unauthorized user ever approve a payout over $10,000?" or "Are any clauses mutually contradictory?". Required with clauses.
ir:
type: object
description: 'Formal IR, solved with zero LLM calls: {variables:[{name,type:bool|int|real,min?,max?}], constraints:[{id,expr,source?}], query:{mode:possible|always|consistency,formula?,source?}}. Expressions are JSON ASTs: {op:"var",name}, {op:"num",value:"3/4"}, {op:"true"|"false"}, and {op,args} for not, and, or, implies, iff, ite, =, !=, <, <=, >, >=, add, sub, neg, mul (one side constant). Numbers are exact strings.'
budget:
type: object
additionalProperties: false
description: Optional lower step budgets.
properties:
maxConflicts:
type: integer
minimum: 1
maximum: 300000
description: Lower this step budget (default and hard cap 300000).
maxPropagations:
type: integer
minimum: 1
maximum: 60000000
description: Lower this step budget (default and hard cap 60000000).
maxPivots:
type: integer
minimum: 1
maximum: 2000000
description: Lower this step budget (default and hard cap 2000000).
maxSplits:
type: integer
minimum: 1
maximum: 5000
description: Lower this step budget (default and hard cap 5000).
maxSolves:
type: integer
minimum: 1
maximum: 2000
description: Lower this step budget (default and hard cap 2000).
maxWork:
type: integer
minimum: 1
maximum: 40000000
description: Lower this step budget (default and hard cap 40000000).
maxMillis:
type: integer
minimum: 1
maximum: 25000
description: Lower this step budget (default and hard cap 25000).
example:
clauses:
- id: C1
text: Any payout request may be approved by a manager.
- id: C2
text: Payouts above $10,000 require approval by a director.
- id: C3
text: A manager is never a director.
query: Can a payout above $10,000 be approved by a manager?
responses:
'200':
description: Paid result with provenance
content:
application/json:
schema:
type: object
properties:
data:
type: object
required:
- deterministic
- headline
- nextStep
- status
- verdict
- mode
- confidence
- result
- audit
properties:
deterministic:
type: boolean
description: True when no LLM touched the verdict path (formal IR input).
headline:
type: string
description: The answer in one or two sentences, rendered from the solver result (witness values or conflicting clause ids).
nextStep:
type: string
description: What to do with this result.
status:
type: string
enum:
- SAT
- UNSAT
- UNKNOWN
verdict:
type: string
enum:
- POSSIBLE
- IMPOSSIBLE
- INVARIANT_VIOLATED
- INVARIANT_PROVED
- CONSISTENT
- INCONSISTENT
- UNKNOWN
- TRANSLATION_DISAGREEMENT
mode:
type: string
enum:
- possible
- always
- consistency
confidence:
type: string
enum:
- high
- medium
- low
result:
type: object
required: []
properties:
model:
type: array
description: Counterexample or witness; verified by exact evaluation against every original constraint.
items:
type: object
required:
- name
- type
- value
properties:
name:
type: string
type:
type: string
enum:
- bool
- int
- real
value:
description: true/false for bool; exact rational string such as "7" or "-3/2" for int and real.
core:
type: object
required:
- clauses
- minimal
properties:
clauses:
type: array
items:
type: string
minimal:
type: boolean
vacuous:
type: boolean
description: True when the clauses are contradictory on their own, so any query answer holds vacuously.
statement:
type: string
description: What was proved, rendered from the formal IR by code.
exhausted:
type: string
description: Which step budget ran out when status is UNKNOWN.
translation:
type: object
required:
- llmCalls
- candidates
properties:
llmCalls:
type: integer
description: 'Model calls attempted: one fast vocabulary call, then one standard and one deep formalization.'
vocabulary:
type: array
items:
type: object
required: []
properties:
name:
type: string
type:
type: string
min:
type: string
max:
type: string
candidates:
type: array
items:
type: object
required:
- tier
- usable
- provider
- model
- verified
- dropped
properties:
tier:
type: string
usable:
type: boolean
description: False when nothing of this translation could be grounded; its drops are still listed.
provider:
type: string
model:
type: string
ir:
type: object
verified:
type: array
items:
type: object
required: []
properties:
clauseId:
type: string
quote:
type: string
formula:
type: string
dropped:
type: array
items:
type: object
required:
- kind
- reason
properties:
kind:
type: string
reason:
type: string
status:
type: string
verdict:
type: string
result:
type: object
required: []
properties:
model:
type: array
description: Counterexample or witness; verified by exact evaluation against every original constraint.
items:
type: object
required:
- name
- type
- value
properties:
name:
type: string
type:
type: string
enum:
- bool
- int
- real
value:
description: true/false for bool; exact rational string such as "7" or "-3/2" for int and real.
core:
type: object
required:
- clauses
- minimal
properties:
clauses:
type: array
items:
type: string
minimal:
type: boolean
vacuous:
type: boolean
description: True when the clauses are contradictory on their own, so any query answer holds vacuously.
statement:
type: string
description: What was proved, rendered from the formal IR by code.
exhausted:
type: string
description: Which step budget ran out when status is UNKNOWN.
equivalence:
type: object
required: []
properties:
question:
type: string
rules:
type: string
reason:
type: string
distinguishing:
type: object
required: []
properties:
scope:
type: string
assignment:
type: array
items:
type: object
required:
- name
- type
- value
properties:
name:
type: string
type:
type: string
enum:
- bool
- int
- real
value:
description: true/false for bool; exact rational string such as "7" or "-3/2" for int and real.
first:
type: boolean
second:
type: boolean
note:
type: string
audit:
type: object
required:
- solver
- version
- algorithm
- budgets
- stats
- inputHash
- irHash
properties:
solver:
type: string
version:
type: string
algorithm:
type: string
budgets:
type: object
stats:
type: object
inputHash:
type: string
irHash:
type: string
_provenance:
type: object
description: C2PA-aligned manifest and W3C VC 2.0 (eddsa-jcs-2022) issued by the hub DID; verify at POST /api/v1/verify-provenance
required:
- data
- _provenance
'400':
description: Invalid request (no payment consumed)
content:
application/json:
schema:
type: object
properties:
error:
type: string
code:
type: string
'401':
description: Invalid X-API-KEY
content:
application/json:
schema:
type: object
properties:
error:
type: string
code:
type: string
'402':
description: Payment required or invalid
content:
application/json:
schema:
type: object
description: x402 v2 PaymentRequired (also base64 in the PAYMENT-REQUIRED header)
properties:
x402Version:
type: integer
error:
type: string
code:
type: string
resource:
type: object
accepts:
type: array
items:
type: object
extensions:
type: object
'502':
description: Upstream failure; the payment is released or not settled
content:
application/json:
schema:
type: object
properties:
error:
type: string
code:
type: string
tags:
- Prove Contract Logic
components:
securitySchemes:
x402:
type: apiKey
in: header
name: PAYMENT-SIGNATURE
description: x402 v2 payment payload (base64) sent after a 402 challenge
apiKey:
type: apiKey
in: header
name: X-API-KEY