A real counterexample from the order-management example, rendered by polyviz. Same inputs, same diagram, every time — no model runs at check time or at render time.
Run it yourself →AI now writes a growing share of the stateful code your systems depend on — workflows, control logic, anything with a "mode." That's exactly the code humans are worst at reviewing by eye: the dangerous bugs live in combinations that are hard to predict and easy to leave untested. Cognitive Fab brings deterministic, exhaustive verification to that code, so your team gates it on every change instead of trusting it on faith.
This is the code layer of the stack. See how it sits under expertise, governance, workflows and simulation →
A real counterexample from the order-management example, rendered by polyviz. Same inputs, same diagram, every time — no model runs at check time or at render time.
Run it yourself →Review catches what a reviewer thought to imagine. It doesn't reliably catch the interleaving that's hardest to picture in advance — the DNS race condition no test enumerates and no reviewer sees, until it's already in production. That's not a hypothetical: it's the exact class of bug that pushed Amazon and Microsoft to formally verify their most critical infrastructure.
Amazon engineers wrote TLA+ models of S3 and DynamoDB to catch design defects in reachable states that testing and code review couldn't reach — the kind of defect that only shows up once you check every reachable state, not the ones a person happens to think of.
Microsoft did the same for Azure Cosmos DB. In both cases, the fix wasn't more review — it was exhaustive, deterministic checking of the state machine underneath the service.
That precedent still asks a team to learn a separate modelling language and keep a second description of the system in sync with the code. Polygraph removes the second description: the spec is ordinary code, checked the same way.
And it's not just Amazon and Microsoft. MongoDB, Elastic, Datadog, PingCAP, Yandex, and dozens of others reach for the same class of tool once review by eye stops being enough.
Ref: Newcombe et al., "How Amazon Web Services Uses Formal Methods," CACM 2015; Microsoft Azure Cosmos DB TLA+ verification; a crowdsourced list of companies using formal methods.
A career spent on stateful systems you can trust: a 1987 Ph.D.; the software engineer and material scientist behind the IMSC closed-loop control project at Hughes Research Labs; chief architect of the NEC Boston Technology Center, leading the design of one of the first business-process engines; and a contributor to the B2B and web-services standards that formalized how systems coordinate — ebXML BPSS, WS-TX, and XML DSig.
What's different now: the spec is ordinary code — no specialist team required to write the math.
A verification-gated lifecycle for the code AI agents now write. Code generation is solved — trust is the bottleneck. Agents already write large amounts of stateful code, the kind hardest to get right, and no human can enumerate every reachable state by eye. The dangerous bugs hide in combinations that are hard to predict and easy to leave untested.
Trust blindly
Trust by construction
Plugins to a coding agent. Every step the agent takes, a deterministic gate checks — no model needed at check time.
Where each tool fires across the development lifecycle, the artifact family they all speak.
Polygraph installs as a Claude Code plugin in two commands. Then point it at the DAAO demo — a dual-authorization action order: two distinct approvers inside a time window, two effects, each exactly once — and ask for the one thing review can't give you: the shortest path to the bug.
# add the marketplace, install the plugin /plugin marketplace add cognitive-fab/polygraph /plugin install polygraph@polygraph
git clone https://github.com/cognitive-fab/polygraph-demo-daao
daao/verify/, make a copy with the distinct-approver guard removed, and run the Polygraph gate on both. Show me it clears the clean build and, on the buggy one, returns the shortest path to a state that violates the two-person rule — the reproduction — without me writing a test.”Advisory, training and hands-on work on the code your team ships with AI, from the author of the SAM pattern — not a menu, a map: pick a corner, or blend a path across it.
SAM v2 contracts, the invariants that matter, and counterexamples kept as regression tests — worked hands-on against machines your team already owns.
half-day to two-day · remote or on-site 04 · BUILDWe wire the gate into your pipeline with your team — contracts written, invariants elicited, the merge gate blocking, and deploys checked against live fleet state.
scoped build · your stack and your CI 01 · ASSESSWhere the stateful code your team ships is trusted rather than checked, which machines carry the most combinatorial risk, and what to gate first.
fixed scope · written assessment + roadmap 03 · EMBEDGates embedded in your lifecycle, and design reviews of your hardest state machines on call — including the version changes that have to survive a live fleet.
monthly retainer · continuousA 30-minute conversation about where AI-written code is quietly accumulating risk in your systems — and whether verification is the answer.