Dependently Typed World Models

World models

The broad strokes: a history of machine imagination

The phrase world model has led several lives. In the age of control theory, it belonged to equations that marched a system from one instant to the next. In cognitive science, it suggested an inner picture of the world, the quiet mental staging ground on which creatures decide whether a rustle in the grass is wind, prey, or danger. In machine learning, the phrase has lately become more theatrical still. A world model is now often a learned simulator, a synthetic sense of how scenes, rewards, and hidden dynamics unfold over time.

The attraction is easy to understand. A system that can imagine futures before it spends a real move in the world may learn faster, plan further, and seem less like a reflex machine than an actor who has at least read the next scene. A world model gives decision-making a stage. It lets an agent try on possible futures, discard the awkward ones, and proceed with the unnerving calm of something that has already rehearsed the moment.

Their glamour comes from a double promise. One promise is practical: better performance, fewer wasted actions, more foresight. The other is interpretive. A world model seems to offer a peek at what the system believes the world to be. If it can reconstruct the scene ahead, anticipate the arc of reward, and carry a durable inner state from moment to moment, then it begins to look less like a statistical gadget and more like a point of view.

A local specimen

What a serious world-modeling stack tends to look like in practice

When world models leave the paper and enter the workshop, they become less like singular inventions than like neighborhoods. One part of the system learns the look and motion of things. Another samples possible futures. Another keeps score. Another compares the dream with the day. Still another tidies the peculiar manners of each environment so the whole affair does not collapse into ad hoc exception. What emerges is not a single trick but an ecology.

The rhythm of the thing is almost literary. A planner begins with the latest glimpse of the world, remembers what was just done and what it cost or earned, fans out a cloud of possibilities, and asks, with remarkable patience, what each one would bring. It then returns to the most promising line of play and narrows its attention there. This is not reaction in the old stimulus-and-response sense. It is deliberation conducted inside a provisional fiction.

At the end there is often a revealing double entry: what actually happened, and what the model thought would happen. The world and its understudy are kept side by side. That pairing is the moral center of the enterprise. Reality sits in one hand, prediction in the other, and the discrepancy between them is not merely an error term but a lesson.

One of the chastening discoveries of the field is that the smell of reward is not enough. Systems that learn only the shape of payoff often become brittle, opportunistic, a little too pleased with themselves. Systems that learn more of the world's actual texture—its surfaces, continuities, occlusions, and transitions—tend to explore more wisely. A useful world model, then, is not merely a reward oracle. It must keep enough of the world's grain to support curiosity.

Explanatory power

What world models explain, and what they often leave implicit

For all their allure, ordinary world models often explain in the wrong register. They can tell us which futures looked attractive, which scenes were reconstructed crisply, which hidden states remained stable under a rollout. What they are worse at telling us is what must remain true regardless of how the story unfolds. They are good with likelihood and weak on legitimacy.

This is where many contemporary systems become eloquent and vague at once. The model can say, in effect, “I expect the future to look like this.” What it cannot easily say is, “Only futures of this permitted shape may even be entertained.” The rules that matter most—about provenance, ownership, budgets, permissions, or scope—are often kept elsewhere, in policies, monitors, comments, and human caution. They hover around the model rather than living inside its understanding of the world.

Dependent type theory

How dependent types change the conversation

Dependent type theory begins from a severe but fruitful premise: the shape of a thing may depend on what the thing actually is, and proof need not arrive afterward like a chaperone. It can travel with the program from the start. Instead of keeping a latent state and hoping later to certify it, one can keep the state together with evidence that it has been properly formed.

In a system such as Rocq, software becomes constructive in the plainest meaning of the word. An object is not just a value; it may be a value accompanied by the evidence required to belong where it claims to belong. A planner, then, need not be merely a function from history to action. It can be a function from well-typed histories to actions whose obligations are partly settled in advance.

For world models, the gain is immediate. Latent state no longer has to drift about as a sealed bag of tensors sustained by faith. It can be recast as a state with lineage, conditions of use, and preserved guarantees—a memory that knows not only what it contains, but why it may be trusted.

A gentler bridge

First, teach the model to keep its own receipts

Before we ask a model to reason about sprawling systems, we can ask something smaller and more human of it: do not make claims you cannot carry. If a plan says it lasts five steps, let those five steps be present. If a context says it is authorized, let that authorization arrive in the same bundle. In Rocq, this lands less like a metaphysical leap than like old-fashioned editorial discipline.

Once that habit takes hold, the mood of the system changes. Safety is no longer a memo taped to the side of the pipeline, waiting for an auditor at the end. It becomes part of what the object is. The center of gravity shifts from "verify later" to "build it so that certain mistakes never come into being."

From Coq Require Import List Arith.
Import ListNotations.

Record CheckedRollout := {
  horizon : nat;
  actions : list nat;
  horizon_matches : length actions = horizon
}.

Definition single_action (a : nat) : CheckedRollout :=
  {| horizon := 1;
     actions := [a];
     horizon_matches := eq_refl |}.

It is a tiny example, almost childlike, and that is precisely why it matters. It shows, in miniature, how claims can be made explicit and inseparable from state itself. And once we can do that for one object, we are ready for the next question: what happens when many such objects must be combined without losing their boundaries?

The Rocq bridge

Partial commutative monoids as a semantics of resource

Once that introductory discipline is in place, the next question arrives naturally: what happens when the state is no longer singular, but fragmented across tools, memories, caches, and actors? This is the moment to borrow a grammar from formal verification: partial commutative monoids, or PCMs. They arise where one must reason about pieces of state that may be combined only when they truly belong together.

The algebra is spare and exacting. There is a notion of validity, a way of joining compatible pieces, a neutral element, and rules that guarantee composition behaves as advertised. From that compact kit one can describe memory as separable fragments, histories as traces that accumulate without confusion, and records that combine lawfully only under stated conditions.

That is precisely what a serious world model tends to lack. A learned simulator knows how to combine predictions numerically; it is far less fluent in combining responsibilities. PCMs suggest a way to make boundaries first-class: which observations belong where, which trace fragments may be joined, which cached beliefs are compatible, and when the system is trying to merge things that should have remained apart.

Illustrative Rocq sketches

Small constructive examples from the ground up

The snippets below are intentionally small. They are less blueprints than glimpses—little windows onto a style of thought in which a model is not merely predictive, but answerable.

From mathcomp Require Import ssreflect ssrbool ssrnat seq.
From pcm Require Import pcm.

Section TypedWorld.
Context {State : pcm}.

Record WorldModel := {
  observe : State -> seq nat -> State;
  imagine : State -> seq nat -> State;
  admissible : State -> Prop;
  observe_ok : forall s frame,
    admissible s -> admissible (observe s frame);
  imagine_ok : forall s actions,
    admissible s -> valid (imagine s actions)
}.

End TypedWorld.

The important move is not syntactic but moral. The model is introduced together with the conditions it must continue to honor. Safety is not appended after the fact. It enters with the cast.

From mathcomp Require Import ssreflect ssrbool ssrnat seq.
From pcm Require Import pcm natmap.

Record rollout := {
  trace : history nat;
  horizon : nat;
  horizon_pos : horizon > 0
}.

Definition extend_trace (r : rollout) (t reward : nat) :=
  if t == 0 then None
  else if valid ((t \-> reward) \+ trace r)
       then Some {| trace := (t \-> reward) \+ trace r;
                    horizon := horizon r;
                    horizon_pos := horizon_pos r |}
       else None.

Here a rollout is not just a sequence of events but a sequence with standing. It carries evidence about its horizon, and it grows only when the next fragment can be joined, cleanly and lawfully, to what is already known.

From mathcomp Require Import ssreflect ssrbool.
From pcm Require Import heap.

Definition sensor_write (p : ptr) (v : dynamic id) (h : heap) :=
  if p == null then Undef else upd p v h.

Lemma sensor_write_preserves_nonnull p v h :
  p != null ->
  sensor_write p v h != Undef.
Proof.
move=> p_nonnull.
rewrite /sensor_write p_nonnull.
case: h=> //= fm pf.
by case: decP=> // /eqP.
Qed.

A deployed system would, of course, be more elaborate than this toy example. Still, the pattern is plain enough: sensing, caching, and acting can be treated as resource transitions with visible terms. An action need not rest on anonymous confidence. It can be required to show its receipts.

Putting the ideas together

How dependent type theory could give world models new purpose

Taken together, these traditions suggest a world model with a more serious civic life. Not merely a predictor of pixels. Not merely a scorer of rewards. Rather, a system able to say: this state was assembled lawfully; this imagined trajectory respects the limits under which it was formed; this action depends only on observations whose standing is still intact; this explanation is not a retrospective story but a checked witness.

Such a model would be especially powerful wherever the world is made not only of physics but of permissions, scopes, obligations, and revocations—multi-agent operations, data systems, policy-constrained automation, secure tool use, financial execution. In such settings, legality is not an afterthought. It is part of the environment.

Security implications

Why this matters for the security of AI and ML systems

None of this amounts to invulnerability. It amounts to a different kind of discipline. Instead of hoping that monitoring will catch dangerous behavior after the fact, one begins to shape in advance the kinds of behavior the system is even permitted to represent and execute.

Closing

A stricter imagination

World models began as a way to let machines picture the road ahead. Dependent type theory suggests that the road, the traveler, and the permission to travel might belong to the same description. The attraction of that union is not that it makes AI less ambitious. It is that it makes ambition answerable.

A dependently typed world model would not abolish error, policy, or judgment. It would simply demand that more of a system's assumptions appear in public, in machine-checked form. And that may be the most compelling promise here: not perfect foresight, but a machine imagination less free to wander and more obliged to answer for what it knows.