State Machine Model Checker
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.
What you get
A mutex, payment flow, or consensus step with a race is found as an exact step-by-step trace before it ships, and a clean result is an exhaustive proof over the modelled state space, not an LLM opinion.
Call it
Send the JSON body below to https://agents.writerslogic.com/api/v1/check-state-machine. An unpaid request answers 402 with the price and how to pay; a request that fails with a 5xx status is not charged.
curl -i -X POST https://agents.writerslogic.com/api/v1/check-state-machine \
-H 'content-type: application/json' \
-d '{"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)"}]}}'
Input
| Field | Type | Required | Description |
|---|---|---|---|
spec | object | no | 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 | string; length 0..30000 | no | Natural-language workflow or protocol; translated to a spec by an LLM, with each transition quoted from the text. |
code | string; length 0..200000 | no | 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 | array<string; length 0..500>; max 20 items | no | Properties to check, in plain language (with description or code only). |
options | object | no |
Example request body
{
"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)"
}
]
}
}
Result
The response is { "data": ..., "_provenance": ... }. data carries these fields; _provenance is a signed W3C Verifiable Credential with a C2PA-style manifest, checked free at POST /api/v1/verify-provenance.
| Field | Type | Required | Description |
|---|---|---|---|
deterministic | boolean | yes | True when no LLM touched the verdict path (formal spec input). |
verdict | string; one of "PASS", "FAIL", "INCONCLUSIVE" | yes | 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 | string; one of "high", "medium", "low" | yes | high for exhaustive results on a formal spec; medium when the model was translated from text; low when inconclusive. |
headline | string | yes | One sentence: the verdict and, on failure, the shortest counterexample path. |
failures | array<object> | yes | Violated properties with the counterexample as a readable path of process.transition steps, an optional repeating cycle (liveness), and the final state. |
nextStep | string | yes | What to do with this result. |
status | string; one of "VERIFIED", "VIOLATED", "BOUNDED", "INCOMPLETE_TRANSLATION", "TRANSLATION_DISAGREEMENT" | yes | |
summary | string | yes | |
exhausted | boolean | yes | True when the whole state space was explored. |
budgetHit | one of | yes | |
properties | array<object> | yes | |
stats | object | yes | |
model | object | yes | |
audit | object | yes | |
translation | one of | yes | |
explanation | one of | yes |
Pay and connect
Available through: x402 (USDC on Base), MCP, RapidAPI, Apify.
Machine-readable
- This agent as JSON (schemas, example, OpenAPI operation)
- Free signed sample response
- OpenAPI 3.1 · Catalog · Index of every agent