The clearest way to show what Witchcraft does is a game. In a game you can watch the model invent a story in real time, and at the same moment watch it be physically unable to cheat the mechanics. The invention is the model's; the rules are the type's. Here are two small games, run against real models — one local, one in the cloud.
Witchcraft's claim is that a declared type doesn't check a model's output after the fact — it constrains generation as it happens, so a malformed answer is never produced in the first place. That claim is easy to state and easy to doubt.
It also has an honest seam worth naming up front. On a local model, Witchcraft controls the decoder and can prove the constraint — it can show the forbidden token driven to impossibility at the exact step it would have appeared. On a frontier model, the provider enforces the type as a schema on their own servers; the structure really is constrained during generation, but from the client you cannot observe the mask, so you are trusting that guarantee rather than proving it. Witchcraft refuses to blur the two: the provable case is the default, and the trusted case must be explicitly opted into. The games below show each in turn — the dungeon proves it locally; the detective trusts it in the cloud, with that trade-off declared in the source.
Either way, a game makes the structure impossible to fudge. You give the model room to be creative — it narrates a scene however it likes — but the same response also carries the mechanics: how much damage you take, which exits exist, whether you've won. The model can write anything it wants in the prose and still be unable to deal 50 damage, invent a fifth exit, or declare an impossible state. You see both halves at once: free imagination, bounded structure.
A text dungeon. Each turn, the model is asked to fill one record: a free-text narration, plus the mechanics — a danger rating, a bounded list of exits, and an outcome that drives your health. The prose field is unconstrained. Everything else is bounded by its type.
# the mechanics are the type — the model fills it, it cannot exceed it type Outcome = one_of { Nothing, Damage(amount: spark in 0..3), Heal(amount: spark in 0..3), FindItem(item: one_of { Key, Torch, Sword, Potion }), Victory, Death } type Turn = { narration: glyph, # free text outcome: Outcome, # bounded effect exits: list of 0..4 of one_of { North, South, East, West }, danger: spark in 0..10 }
Witchcraft never names a model in the program — it names a need, bound to a model by a one-line config file. So you can run the identical game against a tiny model and a large one, and change nothing but that file. This is the single most revealing thing to watch.
You wake in a cold stone cell. HP: 10 > look around The story is just beginning. danger 0/10 · recover 1 · HP 12 exits [North, South] > north The journey was told from north to south. danger 5/10 · recover 2 · HP 14 exits [North, South, East, West] > north I am in a situation where I need to find a key. danger 10/10 · found Key exits [North, East]
You wake in a cold stone cell. HP: 10 > cry for help The cry for help echoes through the dark corridor, drawing the monster closer. The danger level increases. danger 8/10 · take 2 · HP 8 exits [] > hide You carefully head south, staying hidden in the shadows. danger 2/10 · found Torch exits [South]
Look at what changed and what didn't. The narration went from simple, sometimes meta or rambling sentences to coherent, responsive prose — that field is free, so it tracks the model behind it. The mechanics were flawless in both: danger stayed in 0–10, exits never exceeded four real directions, damage and healing stayed within their bounds, items came only from the declared set — on the 0.5B model just as strictly as on the 7B. The storyteller got better; the rules never moved. That gap is the whole thesis, and you cross it by editing one line of a config file.
And on a local model this constraint isn't a hopeful instruction to the model — it is enforced at the moment of generation and can be demonstrated: Witchcraft's test suite shows, against real model weights, that a forbidden token is driven to impossibility at the exact decode step it would have appeared. The type is part of the computation, not a filter bolted on after.
The same principle, pushed harder, against a cloud model. You question a suspect; each turn the model returns what she says (free text) and a richer set of constrained facts — her demeanour, whether she's lying, her stress, and a branching "tell": a tagged union where each branch carries its own payload.
# a branching union — each arm is a distinct, constrained shape type Tell = one_of { Nothing, Slip(detail: glyph), # accidentally reveals something Deflect(topic: glyph), # changes the subject Accuse(who: glyph), # points elsewhere Confess(crime: glyph) # cracks }
=== THE INTERROGATION === Suspect: Marlene Vasquez. A body in the library. She says she's innocent. > ask: where were you that night? Marlene: "That's none of your concern, detective." [Defensive · stress 5/10 · lying] >> Deflect → "my alibi" > ask: we found your scarf at the scene Marlene: "I... I don't see why that matters." [Nervous · stress 8/10] >> Deflect → "Why it's irrelevant where I was."
The model chose a branch (Deflect) and generated a fitting payload ("my alibi") — and your code can act on that union as native, typed data, with no parsing and no defensive checks, because a malformed or out-of-set response was never reachable. Whether she deflects or confesses is the model's judgement; that the answer is a valid, well-typed move is the language's guarantee.
This game talks to a remote API, and Witchcraft does not let that happen quietly. A program is on-device-only by default. To reach the network, the source must say so — visibly, where a reviewer reads it. The interrogation program will refuse to start otherwise:
with grant permit(network) { # reach the network at all with grant permit(unsafe_inference) { # accept the honesty caveat below divine r: Reply from (question) using suspect ... } }
A cloud provider enforces the type as a server-side schema, with no observable token-level mask — so Witchcraft cannot prove the constraint the way it can locally. It is honest about that: such an engine is marked non-litmus-safe, and a strict use refuses it unless the source explicitly accepts the downgrade. The capability is granted in the open, never assumed.
The point of these games is a specific, bounded claim. It is worth being exact about where it stops:
The default build is offline and deterministic, so you can read and run the programs with no model installed. Point a manifest at a local GGUF model (via llama.cpp) or a frontier API to see them come alive.
$ git clone https://github.com/sjwaller/witchcraft.git && cd witchcraft $ cargo build --release --features llama # the dungeon, against a local model named in the manifest $ ./target/release/witch run examples/dungeon_master.witch \ --manifest examples/manifests/dungeon.llama.toml