WhippleScriptThe division of the tools
TLA+ covers the distributed properties and the lifecycle. Maude covers the rule system and the compiler. Lean carries the proofs that need an inductive argument, such as non-interference.
For developers
A coordination language for AI workflows.
WhippleScript treats an agent workflow as a durable program. Its decisions are deterministic. Its external work has an explicit lifecycle. Its authority and its dataflow can be checked before it runs.
research-request.whip
workflow ResearchRequest agent researcher { provider fixture profile "researcher" capacity 2 } rule investigate when Request as request when researcher is available => { tell researcher "Research {{ request.question }}" }
Read the program
Rules react to durable facts. They do not perform work.
The when clauses select a ready combination of facts. The rule is pure. It can inspect those bindings and decide what the workflow requests next. It cannot make a provider call, write a file, read the clock, or perform network input and output while it matches.
In this example the rule records a request for an agent turn. That request becomes a durable effect. A worker executes the effect later. Its outcome is completed, failed, timed out, or cancelled, and the runtime records that outcome into the same history. Another rule matches the outcome and continues the workflow.
This division is deliberate. The policy that selects work can be replayed. The fallible work has an explicit lifecycle that you can inspect, retry, cancel, or escalate.
The kernel
One durable record, advanced in two different passes.
A WhippleScript instance is not a process that holds some state. The instance is the state. Facts, effect requests, effect runs, approvals, failures, program versions, and terminals live in an append-only store. Commands and workers advance that record.
1Rule pass
→Match the facts that the instance holds now. Lower a ready rule into consumed facts, new facts, effect requests, dependencies, and an optional terminal.
2Atomic commit
→Commit that lowering in one transaction. No other rule sees a half transition. An invalid payload commits nothing.
3Effect worker
Execute a pending effect and record its outcome. The outcome is now ordinary workflow state for the next rule pass.
Why this shape?
AI work is delayed and fallible. A model can fail hours after its request. A person can answer tomorrow. A provider can be retried after a restart. Separate deterministic rule evaluation from effect execution, and those cases become part of the language. Otherwise they become hidden callback logic in an application.
Types describe time as well as data
An effect result does not exist until the effect settles.
The type system describes facts, workflow input and output, failures, and effect outcomes in one program model. If a rule requests an agent turn, the compiler knows that the turn can complete, fail, time out, or be cancelled. The result binding exists only inside an after block that observes one of those outcomes.
This prevents a common failure in agent systems: code that assumes an answer exists because a request occurred. A workflow cannot read an effect result before the runtime records it. It cannot complete with a field that it never produced. It cannot silently omit a member of a closed outcome family.
after turn completes as result { complete output { answer result.text } }
The consequence is not better diagnostics only. The possible states of the workflow, and its delayed transitions, stay legible as the workflow grows.
Bounded coordination
Concurrency, waiting, and shared work are visible in the source.
The language has no arbitrary control flow. There is no for loop, no while loop, and no exceptions. To branch, use case with pattern matching. To fan out, let a rule fire one time for each matched fact. To sequence steps, use a then chain, which desugars to the same rules.
WhippleScript rejects recursive workflow invocation and recursive pattern expansion. It requires an explicit shape for the resources that otherwise turn an agent system into an unbounded background process: agent capacity, leases, counters, timers, budgets, and the waits for a person. A tree of agent tools must be acyclic and locally convergent, so a turn never blocks for an unlimited time.
The language does not claim to prove general termination. It makes the structures that govern ongoing work explicit, it rejects the known unbounded forms, and it checks that a workflow has a path to its declared completion or failure contract. A workflow that runs continuously by design carries an explicit tag. That is a more useful promise than the claim that an agent loop is safe because its prompt says that it should stop.
Information-flow control
Labels follow the data, including into model context.
A governed environment labels the real resources, not the variables in one workflow, on a confidentiality axis and an integrity axis. The compiler derives the label of a value from the resources that it passed through. The compiler then checks each later sink.
CONFIDENTIAL SOURCECustomer record
→GOVERNED EGRESSCleared provider
→PUBLIC SINKReviewed reply
Confidentiality answers who may read a value. If only Operator may read a customer record, that value cannot go to a public channel, cannot return to an uncleared caller, and cannot enter the context of a provider without Operator clearance.
Integrity answers what may influence a value or an action. Material from the web, an email, or an uploaded document cannot silently affect a record, a decision, or a release with more trust. This is the answer to prompt injection at the level of the language. The model may read untrusted content. That content gains no authority because it is inside a prompt.
redact customer keep [id, status] as safe complete result { who safe.id state safe.status }
redact is a projection, not a promise. The resulting value has the retained fields only, in its static type and at run time. When a workflow must cross a confidentiality or integrity boundary, it uses an explicit declassified or endorsed coercion. An output schema bounds the crossing, a signed governance grant permits it, and the guarantee report lists it as part of the trusted surface.
The formal layer
The claims are executable, and each one can fail.
The repository holds 93 Maude models, 12 TLA+ specifications, and 12 Lean proofs. The scripts/check-formal-models.sh script runs all of them in CI. Each promise on the guarantees page names the model that carries it.
Every model has a bite
A model also carries its own negative test. The test shows the property fail when you remove the mechanism. A model that cannot fail proves nothing, so a passing suite that never had a bite is not evidence.
Exactly-once, and honest replay
Each effect derives a stable idempotency key from the identity of its firing. A branched timeline and a restored timeline get different keys. Thus a counterfactual run never deduplicates against a real run.
Versioned execution
Change a live workflow without changing its past.
The event history is append-only. The checkpoint and restore commands rewind the working context to a coherent cut across the facts, the files, and the transcript of the agent. The restoration itself is an event on the record. A fork creates a counterfactual branch with a branch-specific effect identity, so work in a hypothetical timeline never deduplicates against production work.
whip revise <instance> candidate.whip --root Workflow --dry-run
Revision is equally explicit. A compatible revision records a new activation and a new epoch. Each effect that the runtime already admitted keeps the version that created it, and each later rule firing uses the new program. That is the correct shape for a workflow that runs long enough to need repair.
Extension without escape hatches
The compiler owns the grammar, the lowering, and the effect lifecycle.
WhippleScript is extensible, but an extension does not get arbitrary control of the runtime. A manifest declares the construct grammar, and the build generates it into the accepted construct table of the parser. A malformed manifest, or a manifest that drifts, fails the build. It does not create a second unreviewed language.
Construct grammar and lowering
Each accepted construct belongs to a known family, scope, and lowering class. Sugar is useful only when it lowers into the ordinary core objects that the kernel already understands: facts, dependencies, workflow terminals, and durable effects.
This keeps the semantic center small. A new spelling does not invent a new execution model. The whip check command prints the result of the lowering, with the reads, the effects, and the dependency edges of each rule.
Package contracts
A package declares libraries, schemas, capabilities, providers, profiles, and typed input and output contracts. A third-party integration executes as an ordinary capability call effect. The runtime checks its output against the declared schema before the output can become a success fact.
A package adds no hidden control flow, no ambient authority, and no path around the effect ledger. The same authority, observability, and information-flow analysis applies at the boundary of the package.
Manifest→Construct catalog→Compiler-owned lowering→Typed durable effect