WritersLogic Verifiable AI Agent Hub Check State Machine API
The Check State Machine API from WritersLogic Verifiable AI Agent Hub — 1 operation(s) for check state machine.
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-check-state-machine-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 Check State Machine API
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: Check State Machine
paths:
/api/v1/check-state-machine:
post:
operationId: state_model_checker
summary: State Machine Model Checker
description: 'Returns PASS, FAIL or INCONCLUSIVE for a finite state machine, protocol, or concurrent routine, with the shortest failing path as readable process.transition steps and a next step. Accepts a formal spec (no LLM), a plain-language workflow, or source code (translated to a spec by an LLM, with every transition quoted from the source and two independent translations compared). A pure TypeScript explicit-state checker explores all interleavings and returns computed verdicts: safety invariants with the shortest counterexample trace, deadlocks, liveness (eventually, always-eventually, leads-to) and livelocks under weak or strong fairness with lasso counterexamples. If the state budget runs out the status is BOUNDED, never a proof.
Price: 2.00 USDC on Base (x402).'
x-x402-price-usdc: '2.00'
x-x402-amount: '2000000'
x-payment-info:
protocols:
- x402
price:
mode: fixed
currency: USD
amount: '2.00'
x-audience: developer
x-sample-url: https://agents.writerslogic.com/api/v1/samples/state-model-checker
security:
- x402: []
- apiKey: []
requestBody:
required: true
content:
application/json:
schema:
type: object
additionalProperties: false
properties:
spec:
type: object
description: Formal spec (zero LLM calls). {vars:{name:{type:'bool'|'int'|'enum'|'array',min,max,values,size|keys,of,init}}, processes:[{name,instances?,fairness?:'none'|'weak'|'strong',transitions:[{name,guard?,updates:[{var,at?,value}]}]}], initWhere?, terminal?, progress?, invariants:[{name,expr}], liveness:[{name,kind:'eventually'|'alwaysEventually'|'leadsTo',p,q?}]}. Expressions are JSON nodes ({var,at?}, {sym}, {param}, {op,args}, forall/exists) or infix strings such as "pc[self] == wait && !flag[1 - self]"; nothing is evaluated as code.
description:
type: string
maxLength: 30000
description: Natural-language workflow or protocol; translated to a spec by an LLM, with each transition quoted from the text.
code:
type: string
maxLength: 200000
description: Source code of a state machine, protocol, or concurrent routine; translated to a spec by an LLM, with each transition carrying its verbatim source span.
properties:
type: array
maxItems: 20
items:
type: string
maxLength: 500
description: Properties to check, in plain language (with description or code only).
options:
type: object
additionalProperties: false
properties:
maxStates:
type: integer
minimum: 1
maximum: 100000
description: State budget (default 100000).
maxTransitions:
type: integer
minimum: 1
maximum: 500000
description: Transition budget (default 500000).
maxMillis:
type: integer
minimum: 1
maximum: 20000
description: Total wall-clock budget in ms for exploration plus liveness analysis (default 8000). On description/code input the three budgets are split evenly between the two translated models.
deadlock:
type: boolean
description: Report deadlocks (non-terminal states with no enabled transition). Default true.
livelock:
type: boolean
description: Report fair cycles that never reach a progress or terminal state; needs a progress or terminal predicate. Default true when the spec has a progress predicate.
explain:
type: boolean
description: Add a plain-language explanation of the computed result (property verdicts, counterexample steps, final state), built from the result itself with no model call. Default false.
example:
spec:
name: flag-mutex
vars:
pc:
type: array
size: 2
of:
type: enum
values:
- test
- set
- crit
init: test
flag:
type: array
size: 2
of:
type: bool
init: false
processes:
- name: P
instances: 2
fairness: weak
transitions:
- name: test
guard: pc[self] == test && !flag[1 - self]
updates:
- var: pc
at: self
value: set
- name: set
guard: pc[self] == set
updates:
- var: flag
at: self
value: true
- var: pc
at: self
value: crit
- name: exit
guard: pc[self] == crit
updates:
- var: flag
at: self
value: false
- var: pc
at: self
value: test
invariants:
- name: mutualExclusion
expr: '!(pc[0] == crit && pc[1] == crit)'
responses:
'200':
description: Paid result with provenance
content:
application/json:
schema:
type: object
properties:
data:
type: object
properties:
deterministic:
type: boolean
description: True when no LLM touched the verdict path (formal spec input).
verdict:
type: string
enum:
- PASS
- FAIL
- INCONCLUSIVE
description: 'PASS: every property holds over the full state space. FAIL: at least one property has a counterexample. INCONCLUSIVE: budget hit or translation incomplete or disputed; never a proof.'
confidence:
type: string
enum:
- high
- medium
- low
description: high for exhaustive results on a formal spec; medium when the model was translated from text; low when inconclusive.
headline:
type: string
description: 'One sentence: the verdict and, on failure, the shortest counterexample path.'
failures:
type: array
description: Violated properties with the counterexample as a readable path of process.transition steps, an optional repeating cycle (liveness), and the final state.
items:
type: object
properties:
property:
type: string
kind:
type: string
path:
type: string
steps:
type: integer
cycle:
anyOf:
- type: string
- type: 'null'
finalState:
anyOf:
- type: object
- type: 'null'
message:
type: string
required:
- property
- kind
- path
- steps
- cycle
- finalState
- message
nextStep:
type: string
description: What to do with this result.
status:
type: string
enum:
- VERIFIED
- VIOLATED
- BOUNDED
- INCOMPLETE_TRANSLATION
- TRANSLATION_DISAGREEMENT
summary:
type: string
exhausted:
type: boolean
description: True when the whole state space was explored.
budgetHit:
anyOf:
- type: string
- type: 'null'
properties:
type: array
items:
type: object
properties:
name:
type: string
kind:
type: string
enum:
- invariant
- deadlock
- runtime
- eventually
- alwaysEventually
- leadsTo
- livelock
status:
type: string
enum:
- HOLDS
- VIOLATED
- UNDECIDED
source:
type: string
counterexample:
type: object
description: Shortest trace for safety violations; prefix plus repeating cycle (lasso) for liveness and livelock violations. Each step lists the process, the transition, its source span (translated input), and the full state.
properties:
type:
type: string
enum:
- trace
- lasso
message:
type: string
trace:
type: array
items:
type: object
cycle:
type: array
items:
type: object
failedStep:
type: object
required:
- type
- message
- trace
required:
- name
- kind
- status
stats:
type: object
properties:
statesExplored:
type: integer
statesExpanded:
type: integer
transitionsChecked:
type: integer
diameter:
type: integer
initialStates:
type: integer
sccCount:
anyOf:
- type: integer
- type: 'null'
nontrivialSccCount:
anyOf:
- type: integer
- type: 'null'
largestScc:
anyOf:
- type: integer
- type: 'null'
required:
- statesExplored
- statesExpanded
- transitionsChecked
- diameter
- initialStates
- sccCount
- nontrivialSccCount
- largestScc
model:
type: object
audit:
type: object
translation:
anyOf:
- type: object
- type: 'null'
explanation:
anyOf:
- type: object
- type: 'null'
required:
- deterministic
- verdict
- confidence
- headline
- failures
- nextStep
- status
- summary
- exhausted
- budgetHit
- properties
- stats
- model
- audit
- translation
- explanation
_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:
- Check State Machine
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