Your staff want to use AI agents on company work. You agree with the goal. You cannot approve it, because you have no way to limit what an agent does with company data. A prompt is not a control. WhippleScript makes the limit a property of the language: you declare your resources and their audiences one time, and the compiler refuses to build any workflow that violates that policy.
You identify the real systems that a workflow may use: data stores, files, channels, model providers, tools, and people. You declare who is cleared to read each one, and what may influence it. Your staff then create and change workflows freely. The compiler applies your policy every time.
You write the policy. Your staff and their agents write the workflows. A workflow cannot widen its own authority, and an author cannot quietly change the policy that constrains him. The policy is signed, and an altered policy invalidates its attestation.
A denied workflow does not deploy. There is no run-time monitor to tune, and no alert queue to triage. You are involved when the organization wants to move the boundary, not each time a person wants to automate a task.
Each governed workflow prints a guarantee report. The report names each resource, each audience, each cleared provider, and each approved exception. Read it before you promote a workflow.
Each model named below is executable. CI runs all of them with the scripts/check-formal-models.sh script. A guarantee on this site is not prose.
No. Under a governance envelope the compiler denies a value to each audience outside its set of readers. This includes the context of a model provider: WhippleScript treats a prompt as a disclosure.
models/maude/infoflow-*.maude · models/lean/Whipple/ReaderSets.leanNo. The compiler denies untrusted data influence over a sink with more trust. The model may read untrusted content, but that content gains no authority by being inside a prompt. The only crossing is an endorsed coercion that a person authorized.
models/lean/Whipple/NMIF.leanNo. The compiler denies data that an attacker controls the ability to steer its own release.
models/lean/Whipple/NMIF.leanYes. A redaction is a projection, not a promise. The retained fields are the only fields in the static type and the only fields at run time.
models/lean/Whipple/Redaction.leanNo. The tree of agent tools must be acyclic, and each tool workflow must be locally convergent. Thus a turn never blocks for an unlimited time. A workflow that runs continuously by design must say so with an explicit tag, and only the root may do it.
models/maude/subworkflow-convergence.maudeNo. Each external action derives a stable idempotency key from the identity of its firing. A retry, a recovery after a crash, and a replay each deduplicate against that key. The customer gets one email, not four.
models/maude/effect-key.maude · models/maude/prefix-replay.maudeNot by default. Each of the three is default-deny and needs an explicit operator grant. The virtual shell has no reach to the operating system and no reach to the network. Network access is an HTTP GET from an allow-list, and it blocks each private and loopback address.
models/maude/script-hard-off.maudeNo. Authority enters a program explicitly and only becomes more narrow. The access of a turn, the authority at the boundary of a child workflow, and the fields that a redaction keeps are each a subset of the authority of the granter. Nothing becomes larger downstream.
models/maude/workflow-authority-attenuation.maude · models/maude/turn-access-grant.maudeYes. The event log is append-only. Each event carries causation and correlation identifiers, so the cause of an action is a query and not a reconstruction. The whip trace --check command replays a run against the conformance model.
Yes. A crossing is a declassified or endorsed coercion, bounded by an output schema, under a signed grant, with a source mark. Each one appears in the guarantee report as part of the trusted surface. An exception is narrow, visible, and checked across every workflow.
Refer to the governance tutorial.In a store that you select: a local database file, or a Cloudflare Durable Object in your own account. A workflow refers to a credential by name and never contains a key. Only the owner of the configuration file can read it.
Refer to the runtime and operations guide.Each governed workflow produces a report. The report shows the resources that the workflow uses, the protections that the compiler checked, the cleared providers and principals, and each explicit exception in the policy.
The runtime then keeps an append-only record of what occurred: the information read, the actions requested, the approvals received, and the actions completed.
crm may not reach an uncleared provider or destination
public-reply receives only public output
approved-model cleared for Operator context
✓ violations caught: 0
We would rather you learn this here than in a pilot.
WhippleScript