Maquina

Explore the Maquina Playground.

Maquina is a formally specified execution model for deterministic, replayable worlds. It describes what exists, where it belongs, which changes are allowed, what each accepted change produces, and how the resulting history can be reconstructed and verified.

The central boundary is simple:

Agents, people, policies, planners, and solvers propose. Maquina determines what those proposals mean, whether they are valid, and what consequences they produce.

This repository is a conceptual foundation. It contains a proof-carrying Lean 4 semantic kernel, runnable downstream game simulations, and a catalog-driven Three.js Playground for Lean-generated traces and command graphs. No implementation has been copied from earlier projects.

Maquina Playground

The Maquina Playground presents Lean-generated scenarios as interactive three-dimensional worlds. It is a projection, never an alternative state-transition implementation:

Resource reservation. The receipt explains Body possession, fuel custody, and process enqueueing.	Queue transition. Active custody remains visible while the process moves into processing.

Scene objects retain their identity across steps. Resources move only when a receipt records a transfer, processes interpolate between queues, and machine mechanisms animate only while their state justifies it. The inspector connects every visible change to accepted effects or a structured rejection.

Lean simulation -> versioned trace -> shared scene document -> Three.js

The Lean exporter owns exact state snapshots, accepted effects, structured rejections, and replay provenance. Games provide only scenarios, vocabulary, and declarative presentation. The scene projector and Three.js renderer contain no Foundry or other game-specific rules.

Command-capable showcases export an optional counterfactual command graph. Enter Command mode to select simultaneously submitted orders, inspect why every candidate is accepted or rejected within the actor's information boundary, watch the scheduler resolve the exact Lean-owned fork, rewind to any prior immutable snapshot, and compare terminal outcomes. The Playground labels every entry as trace, commandable, or trace + command instead of pretending that a fixed demonstration is an interactive world.

Operation Nightglass provides both a canonical trace and mission command forks. Foundry Control Room is commandable from its first snapshot: assign one unique operator Body across two isolated service runtimes, create or cancel backlog, run a productive cycle, take a safe maintenance window, or submit a simultaneous dispatch/departure pair that deterministically conflicts and enters a proved failure/repair path. The static browser never runs either game's rules; every snapshot, assessment, receipt, event, and outcome is generated by Lean.

Operation Veiled Accord adds imperfect-information strategy. Public claims, verified coalition evidence, account-level escrow, information sets, hidden partner commitments, simultaneous sealed reveals, cooperation, exploitation, and betrayal are exported through protocol v4. Candidate availability and redacted explanations factor only through the commander's observation, so the browser cannot use authoritative assessment as a secret-state oracle.

Generate and validate the complete site with:

cd visualizer
pnpm install
pnpm check

See visualizer/README.md for the shared protocol and the steps required to register another game or scenario.

Origin: digital twins as executable worlds

The project began with Maquina: A Theory of Everything for Digital Twins, an earlier vision for building digital twins from a small vocabulary of Objects, Operations, and Machines. The article is conceptual history rather than the current specification, but its central ideas still guide Maquina:

• a useful digital twin is an executable world, not merely a dashboard or static representation;
• computationally irreducible behavior must be explored by running the model, replaying it, and comparing possible histories rather than assuming every outcome has a shortcut;
• possible and impossible transformations should be stated explicitly, in the spirit of Constructor Theory; and
• humans, robots, LLMs, planners, and other agents should interact with one shared world model without becoming hidden sources of authority.

The vocabulary has become more precise as the formal model has developed:

Earlier article	Current Maquina model
Objects	Resources: quantified, measured, unique, bounded, informational, or capability-bearing things.
Operations	Operations and Processes: state changes and resource transformations proposed against explicit requirements.
Machines	Machines, inventories, custody, and typed queues: stateful constructors that schedule and perform accepted transformations.

Accounts locate resources; proposals bind abstract rules to a concrete world; receipts and events make consequences inspectable and replayable. LLMs can help people describe worlds and propose actions in natural language, but the semantic kernel—not the LLM—decides what is valid and what happens next.

Conceptual lineage

Maquina consolidates ideas explored independently across three repositories. This is conceptual lineage, not a code merge.

Source	Contribution to the concept
rozgo/maquina	Typed resources, inventories, event sourcing, replayed projections, knowledge access, and MCP tools for agent interaction.
rozgo/maquina-bevy	Composable resources, queues, universal machines, operations, processes, behavior trees, deterministic time, and simulation through Bevy ECS.
BiomaAI/axionomy	Closed authoritative state, assets and accounts, rates and exchanges, explicit invariants, structured rejection, exact forks, solver-neutral search, and verified replay.

The new Maquina keeps the common thesis while remaining independent of the existing implementations, storage systems, interfaces, and frameworks.

What Maquina is

Maquina is a semantic kernel for systems whose state and changes must be explicit, inspectable, and reproducible. The same model should be usable for:

• operational software;
• industrial and logistics systems;
• games and persistent simulated worlds;
• planning, optimization, and counterfactual exploration;
• human, robotic, and AI-agent coordination;
• auditable automation and formally checked execution.

Maquina is not an agent framework or a solver. It is the authoritative environment those systems act against. An agent can propose an action, a planner can explore a fork, and an optimizer can rank alternatives, but none of them can make an invalid transition valid or mutate authoritative state through a side channel.

Core model

The vocabulary will be refined in Lean before the Rust runtime is designed, but the initial model has the following roles.

Resources

A resource identifies anything that can exist or matter: a physical material, a unique artifact, a fact, a capability, a permission, a condition, a goal, an observation, or a state token. Quantities may be discrete, measured, unique, or composed, while preserving exact identity and units.

Accounts and inventories

An account answers "where?" or "currently held by whom?" It can represent a person, agent, machine, location, organization, scope, or namespace. An inventory is a useful view of the resources held by an account; it is not a separate source of truth. Persistent ownership is not inferred from custody: return provenance is recorded by accepted reservations, while transferable rights may themselves be resources.

At its simplest, authoritative state can be understood as:

State : Account x Resource -> Quantity

Rules, rates, operations, and processes

A rule defines an allowed kind of change. It can declare:

• required and preserved conditions;
• consumed inputs;
• produced outputs;
• actor and account bindings;
• capabilities and permissions;
• capacity, timing, ordering, and uniqueness constraints;
• invariants that must remain true.

An operation changes the condition of a machine or actor. A process transforms inputs into outputs. Both are specializations of explicit transition rules, not permission to run arbitrary hidden mutation.

Proposals, exchanges, and events

A proposal binds a rule to concrete actors, accounts, resources, quantities, and parameters. Assessment is pure: it either returns a structured explanation of why the proposal cannot apply or a complete description of its effects.

Applying an accepted proposal atomically produces a receipt and an immutable event. The event history can reconstruct the same state through replay.

proposal -> assess -> reject(reason)
                   -> accept(effects) -> apply -> receipt + event

Machines and queues

A machine is a stateful processor governed by rules. It may have an inventory, accept work through ordered queues, run one or more processing slots, consume and produce resources, expose operating conditions, and record its evolution.

Queues make ordering, capacity, ownership, cancellation, and collection explicit. Time is supplied by the environment so tests and simulations remain deterministic.

Agents and behaviors

Agents observe the portion of state they are permitted to see and propose actions through the same transition boundary as every other participant. Behavior trees, LLMs, policies, planners, scripts, and human interfaces are replaceable decision systems outside the authoritative kernel.

Projections, observations, and knowledge

Indexes, projections, graphs, dashboards, search structures, embeddings, and knowledge views are derived from authoritative state and events. They may help participants understand the world or choose a proposal, but rebuilding or losing a projection cannot change what is valid.

Current Lean foundation

The checked Lean implementation currently provides:

• exact discrete, measured, unique, and bounded-edition resources;
• canonical account holdings with known-resource and global-supply invariants;
• funded atomic transfers with structured shortfalls, conservation theorems, receipts, and exact holding replay;
• checked debit/credit transformation programs with all-or-none execution and exact replay;
• normalized, machine-independent multi-account transactions with canonical account/resource ordering, complete indexed rejection, exact movement constructors, no rejected successor, and receipt replay;
• capacity-bounded FIFO queues with ordered, unique, monotonic tickets;
• direction-typed machine queues, a machine-wide queue maximum, and monotonic queue identities;
• declarative processes with proof-complete consumed inputs, temporary reservations, active-custody requirements, work, canonical outputs, account bindings, and receipt-derived provenance;
• state-indexed, non-consuming possession requirements checked before operation effects;
• receipt-backed machine custody with aggregate balance locks, exact return sources, monotonic custody positions, and proof-backed active-work dependencies that prevent premature exit;
• a generic declarative operation interpreter with proof-carrying guard acceptance, exhaustive structured guard and possession rejection, and no game-specific transition helpers;
• machine runtimes separated from authoritative account state so downstream applications can own any heterogeneous component topology; generic receipt theorems preserve untouched account balances and custody backing;
• deterministic logical ticks, scheduled application intents, canonical game-owned arbitration keys, snapshot eligibility, and conflict rejection;
• immutable tick events whose accepted receipts replay the complete application state while rejected events replay as identity;
• generic actor identities, structured candidate assessment, deterministic simultaneous command order sets, actor-scoped observation policies, replayable timeline snapshots, and immutable parent-prefix forks;
• a reusable proof-carrying command graph whose nodes own exact-snapshot assessments and whose edges prove accepted action references, exact selected first-tick intents, connected replay-exact paths, unique action choices, accepted-candidate coverage, actor ownership, and complete terminal status;
• universal completion and allocation-delivery contracts with exact receipt coverage, unrelated-balance preservation, and non-reusable collected queue tickets;
• atomic queued and active cancellation with declared return-or-consume input disposition;
• partial output collection with proof-carrying remaining allocations and non-recurring collected labels;
• first-class positive-lot rates and atomic multi-account exchanges with indexed shortfalls, conservation, exact receipts, replay, reversal, and custody-lock-aware execution;
• accepted operation traces carrying a proof that deterministic semantic replay reaches their exact final simulator state;
• proposal-free direct effect receipts that reconstruct holdings by receipt fold and apply exact machine, queue, custody, mode, and counter patches; and
• a Foundry game proving admission-time Body presence, queued versus active Body-session behavior, proof-carrying idle/active operating guards, atomic failure cancellation and repair, queued versus active Labor, one-time collection, queue drainage, custody return, one-job/two-job replay, and workcell contention for one unique Body, plus a commandable Control Room with productive, recovered, backlog, conserved, deferred, and maintained outcomes;
• an Operation Nightglass game proving heterogeneous game-owned composition, deterministic same-tick contention, account-funded ammunition and repair, damage recovery, complete event replay, convoy extraction, actor-view noninterference, and a bounded counterfactual command graph with clean, costly, exposed, and aborted outcomes; and
• an Operation Veiled Accord game proving actor-safe command-surface noninterference, information-set strategy consistency, audience-scoped communication, exact multi-party consent, account-level escrow, actor-unique sealed reveals, and payoff-bearing cooperation and betrayal outcomes.

The proof inventory is summarized in docs/lean-lifecycle-plan.md. Semantics that remain unimplemented or insufficiently general are tracked explicitly in docs/lean-proof-todo.md.

Build and inspect the current reference behavior with:

lake build
lake exe foundry-demo
lake exe nightglass-demo
lake exe veiled-accord-demo

What Maquina enables today

The checked Lean reference semantics and exported browser showcases already:

• define typed resources, capabilities, conditions, units, accounts, and inventories;
• move and transform resources through funded, atomic, replay-exact transfers, transactions, and exchanges;
• describe machines, workflows, queues, processes, operations, guards, and transformations as data;
• assess actions without mutation, report every independent failure, and carry proof-backed acceptance evidence;
• apply accepted actions atomically while rejected actions expose no successor;
• resolve scheduled intents at deterministic logical ticks with explicit conflict ordering;
• record immutable events and reconstruct authoritative application state by replay;
• snapshot timelines, fork exact shared prefixes, simulate bounded futures, and compare terminal outcomes;
• project actor-scoped observations and assess advertised candidate actions through the same authoritative transition boundary;
• construct visible command surfaces only from declared observations, group hidden alternatives into information sets, and keep strategies consistent across indistinguishable states;
• record audience-scoped messages, bind sealed command reveals, require exact multi-party consent, and fund agreements through account transactions; and
• verify foundational safety, conservation, isolation, uniqueness, and replay invariants against the formal specification.

These are executable reference semantics, not yet a production runtime. The remaining layers include:

• generalized authorization and capability-binding policy beyond the concrete actor observation policies supplied by games;
• declared multi-actor goals, cooperation, competition, and planner-facing search beyond finite exported command graphs;
• fairness or liveness contracts for games that explicitly declare such a scheduling policy;
• recursive packs and bundles with canonical expansion proofs;
• persistent, versioned event storage and rebuildable production projections;
• a Rust kernel with exact conformance to deterministic Lean fixtures; and
• APIs, events, MCP, and other adapters that cannot bypass authoritative assessment and application.

Rust and Lean

Maquina starts as two deliberately separate layers.

Lean 4: semantic specification

Lean defines the meaning of Maquina before runtime concerns are introduced. The formal model already covers the current resource/process/machine lifecycle, logical time, deterministic intent resolution, immutable event replay, actor-scoped observations, replayable snapshots, counterfactual forks, and proof-carrying command graphs. The remaining semantic work is to generalize authorization and capability bindings, establish projection noninterference, define optional fairness or liveness contracts only where games declare them, and introduce declared goals and richer multi-actor policy without moving game rules into the kernel.

The current checked foundation establishes substantial portions of the original proof targets:

• valid constructed worlds preserve canonical holdings, known resources, bounded supply, and queue capacity;
• rejected transfer, transformation, and operation APIs expose no successor;
• accepted transfers satisfy funding and catalog preconditions;
• pure inventory programs are all-or-none;
• transfer, transaction, transformation-program, semantic operation, proposal-free direct-effect, and timeline-event replay reach their exact checked successors;
• generic account receipt isolation preserves unrelated runtime custody backing in game-owned compositions;
• scheduled conflicts commit only the canonically winning accepted intents; rejected events replay without mutation; and
• unique resources cannot simultaneously occupy two distinct accounts.

The remaining universal theorems and future semantic layers are intentionally listed in the Lean proof backlog, rather than being implied as already complete.

Lean is the source of semantic truth, not the production runtime. The project may later generate test vectors, executable reference behavior, or checked artifacts that the Rust implementation must satisfy.

Games

The games directory contains formal game simulations built as downstream users of Maquina. They give the semantic kernel concrete worlds to execute and provide proof targets that are understandable as playable rules, rather than isolated formal examples.

Each game owns its domain vocabulary and rules. Concepts such as running, broken, refuel, smelt, or repair belong to a game, while Maquina currently supplies generic resource, queue, process, operation, machine, custody, possession, cancellation, partial collection, rate/exchange, and semantic/direct replay behavior plus a state-agnostic logical timeline. Nightglass demonstrates that radar, battery, convoy, damage, interception, and mission outcomes remain entirely downstream game policy. Veiled Accord likewise keeps routes, claims, evidence meaning, partner policy, trust, betrayal, and payoff functions downstream while exercising generic information, communication, consent, escrow, and sealed-round protocols.

Rust: executable kernel

Rust will eventually provide the production engine, persistence boundaries, projection machinery, simulation APIs, and integration surfaces. The runtime must implement the Lean-defined semantics and demonstrate parity through shared fixtures and conformance tests.

The Rust workspace is intentionally empty today. No crate structure or framework choice should harden before the vocabulary and transition contract are precise.

Architectural boundary

people / agents / policies / planners / solvers
                       |
                       v
                proposed action
                       |
                       v
        +-------------------------------+
        |            MAQUINA            |
        | observe -> assess -> apply     |
        | state + rules + invariants     |
        +-------------------------------+
                       |
                       v
      receipt + event + new observation + trace

Decision systems may use snapshots and forks to reason before proposing a change. Only Maquina applies changes to the authoritative state.

Non-goals for this foundation

This repository does not yet choose or provide:

• code copied from any predecessor;
• a database or event-store implementation;
• an ECS, robotics stack, or production runtime deployment platform;
• an agent runtime, model provider, or training system;
• a universal ontology for every domain;
• compatibility guarantees with existing Maquina, Bioma, or Axionomy data.

Those decisions should follow the formal model rather than define it by accident.

Development sequence

1. Close the remaining explicit Lean proof backlog, including recursive packs/bundles and projection noninterference.
2. Complete authorization and capability-binding policy, then broaden declared goals and multi-actor analysis beyond bounded game-owned command graphs.
3. Stabilize and version the artifact, event, and conformance contracts, then export deterministic accepted and rejected Lean fixtures.
4. Implement a pure Rust kernel and require exact state, issue, receipt, event, and replay parity with those fixtures.
5. Add persistent event storage and rebuildable derived projections.
6. Add optional adapters for APIs, MCP, agents, simulation, ECS, and operational platforms without granting them direct mutation authority.

Repository layout

Cargo.toml          Empty Rust workspace
rust-toolchain.toml Pinned Rust toolchain
lakefile.toml       Lean project definition
lean-toolchain      Pinned Lean 4 toolchain
lake-manifest.json  Reproducible Lake dependency manifest
lean/Maquina.lean   Public root module for the formal specification
lean/Maquina/       Formal model modules and proofs
games/foundry/       Downstream declarations, closed proofs, and runnable trace
games/nightglass/    Heterogeneous scheduled mission, proofs, and runnable trace
games/veiled-accord/  Imperfect-information strategy, proofs, and command game
visualizer/          Maquina Playground, Lean exporter, and shared Three.js UI
docs/                Current proof inventory and explicit Lean proof backlog
README.md           Conceptual overview and current implementation status
.github/workflows/  Rust workspace and Lean build validation

The repository should remain concept-first until the relevant formal vocabulary and proof backlog are stable enough to support each runtime slice.