Praxec’s whole pitch is that the wrong move isn’t blocked — it’s not there to call. Your agent is on a state machine, and the dangerous transition simply isn’t in the list of legal moves at that state. You don’t trust a prompt to keep it in line. You take the option away.
That’s a strong guarantee. It rests entirely on one assumption: that the state machine you wrote is the one you meant to write.
And here’s the uncomfortable part. You can’t eyeball a state machine. A dozen states, fifty transitions, guards on half of them, branches that fork on a context value — read that as YAML and tell me, with a straight face, that nothing is orphaned, that every guard rejects what it’s supposed to, that there’s no state you can enter but never leave. You can’t. Nobody can. So how do you know your guardrail is actually a guardrail and not a gate with the latch off?
Three questions, three commands
Praxec answers this in three steps, each a little stronger than the last. Does it load? Does it behave? Does it hold the properties you care about?
check — does it load?
praxec check is the static pass. It reads the config and proves the structural things: the schema is valid, every transition target points at a real state, every state is reachable, and no non-terminal state is a dead end you can enter but never leave.
$ praxec check --config gateway.yaml
error[unreachable_state]: state 'rollback' is not reachable from initialState
error[dead_end]: state 'waiting' declares no transitions and is not terminal
exit code 1This catches the typos and the dangling pointers — the bugs that make a config wrong on paper. It runs nothing, so it’s the cheapest check you have, and it should be the first thing in CI. But a config that loads cleanly can still misbehave the moment it runs. A guard can be present and still let the wrong input through.
fuzz — does it behave?
praxec fuzz proves the config behaves — and it does it with no real model and no network. Deterministic. It drives the state machine through generated inputs and transition sequences, looking for a move that should have been refused but wasn’t, an input a guard should have caught but didn’t, a workflow that gets stuck. It exits non-zero on a failure, so you wire it straight into CI next to check.
There’s a trap worth naming: fuzzing proves the machine does what the machine says, not that the machine says the right thing. It’ll catch a guard that doesn’t reject what its own schema forbids; it won’t catch a policy you never wrote down. Which is why there’s a third step.
test — does it hold?
For the properties that actually matter to your process — “a deploy is never reachable without a green-CI evidence record,” “the approve move is always actor: human” — you write them down as assertions and run them against the config. This is where you encode intent: not “the machine is internally consistent” but “the machine enforces the specific rule I built it to enforce.”
Trust the guardrail, then verify it
The guarantee — wrong moves are unreachable — is only as good as the graph behind it. check proves the graph is well-formed, fuzz proves it behaves as written, and test proves it behaves as intended. All three run without a model and without a network, which means they run in CI, on every change, in seconds. Your state machines get the same treatment as your code: not eyeballed and hoped over, but verified before they ship.