Platform Overview
mashin is a governed intelligence substrate. That phrase packs in a lot, so this page unpacks it: what the platform is, what each component does, and how they connect.
The big picture
You write machines in MashinTalk, a purpose-built language that compiles to BEAM bytecode. Machines run inside cells, your personal computing environments. Every execution is governed by kore, the formally verified governance kernel, and recorded in a tamper-evident behavioral ledger. You publish machines as krates to kura, the package registry. Cells communicate through kortex, the governed network fabric. You build all of this in koda, the intelligent development environment, which renders its interface through kodex. End users interact with machines through kanvas, the graphical interface layer. Kanon, the governance ledger, records the provenance of every machine version.
Here is how the pieces relate:
You ──→ koda (IDE) ──→ write MashinTalk ──→ compile to BEAM │ ▼ Cell (runtime) ├─ kore (governance kernel) ├─ Behavioral Ledger (execution trace) ├─ kanon (governance ledger) └─ kortex (network fabric) ──→ other cells
Published machines ──→ kura (registry) ──→ pulled into cellsMachines with UI ──→ kanvas (interface layer) ──→ end usersMachines
A machine is the fundamental unit. It is a governed unit of intelligence: a computation that thinks internally and acts externally through a controlled boundary. Every machine has typed inputs, typed outputs, governance rules, and an implementation made of steps. Each .mashin file defines one machine.
Machines are not scripts, notebooks, or agents in the LangChain sense. They are structured programs with contracts. The runtime enforces those contracts. See Machine Anatomy for the full structure.
MashinTalk
MashinTalk is the surface syntax of the mashin language. It uses keyword-hierarchy syntax: structural keywords determine program structure through indentation. No braces, no do...end. The keyword vocabulary is the grammar.
machine email_classifier
accepts subject as text, is required body as text, is required
responds with priority as text category as text
implements ask classify, using: "anthropic:claude-sonnet-4-6" with task "Classify this email by priority and category" returns priority as text category as textMashinTalk is designed to be readable by compliance officers, not just developers. It compiles to BEAM bytecode, is deterministic (one parse tree per program), and is multilingual (the keyword vocabulary can be swapped for other natural languages while keeping the grammar).
Cells
A cell is your mashin environment. It is where your machines live, run, and store their history. Three properties define a cell: it is owned (your machines, your data, your keys), persistent (survives restarts and moves), and networked (connects to other cells, the registry, and the cloud).
The same cell concept works everywhere: your laptop, a Docker container, a Mac Mini, a cloud VM. The code does not change between environments. A machine that runs in your laptop cell runs identically in a cloud cell.
The hierarchy: a machine is a governed unit of intelligence. A cell is where machines live. The substrate is cells networked together via kortex.
See Cells for the full guide.
koda
Koda is the live intelligent development environment. It is not an assistant or chatbot bolted onto an editor. The entire interface is intelligent. You work in projects, books, and sessions, and koda provides context-aware help throughout.
What makes koda different: intelligence is ambient, not invoked. koda’s cognitive operations are themselves mashin machines in the @system/koda/* namespace, so they are governed, auditable, and inspectable. This is the Smalltalk property: the development environment is built from the same primitive as the things it builds.
See koda for the full guide.
kodex
Kodex is the text-first rendering surface where builders work inside koda. It is a character-grid interface with cell types at multiple depth levels: prose (summary), detail (full data), and trace (execution internals). Named from “codex” (bound manuscript), kodex renders execution traces, machine state, and governance decisions as structured text.
Kodex and kanvas are complementary: builders work in kodex, end users interact through kanvas.
kore
Kore is the formally verified governance kernel. It is extracted from Rocq (Coq) proofs and bridged to the BEAM runtime via a NIF. Every governance decision at runtime runs through proved code: 32 modules, 406 theorems, 0 admitted lemmas.
This is what makes mashin’s governance claims provable, not just aspirational. The four Laws of Governed Intelligence are backed by machine-checked theorems. The expressiveness boundary and the governance boundary are mathematically proven to be coterminous: you cannot write a machine that escapes governance because the capability does not exist.
krates
A krate is the distribution unit in mashin. Every machine is a krate from birth: a versioned, signed package with its source, compiled artifact, governance rules, tests, and metadata. You do not “turn a machine into a package.” It already is one.
Krate metadata lives in krate.toml alongside the .mashin file:
[krate]name = "email-triage"version = "1.2.0"description = "Classify and route incoming emails"license = "MIT"
[krate.author]name = "Your Name"Every published krate is immutable, signed with Ed25519, and verified through six cryptographic levels. Krates use semantic versioning. You reference krates by namespace and path: @mashin/actions/http/get (stdlib), @myorg/billing/charge (organization).
kura
Kura is the package registry where krates are published, discovered, and pulled. Every published krate goes through six levels of cryptographic verification: file integrity, artifact identity, publisher authenticity, envelope integrity, registry attestation, and lineage provenance.
Kura supports federation. Organizations can run their own kura instance for internal machines while pulling public dependencies from the main registry.
See Publishing & kura for the full guide.
kortex
Kortex is the governed network fabric connecting cells. When a machine in one cell calls a machine in another cell, the call goes through kortex with governance on both sides: your cell checks that you are allowed to make the call, the remote cell checks that you are authorized to invoke that machine.
Three tiers of networking:
- Local: cells on the same machine, zero configuration
- Organizational: cells within the same organization, deployment-backed
- Cross-organization: cells across organizations, portable governance
The directive interpreter is the networking layer. There is no separate “API gateway” or “service mesh.” Governance and networking are the same thing.
kanvas
Kanvas is the graphical interface layer where machines become reachable to end users. It supports MCP, REST, WebSocket, and webhooks. In MashinTalk, the expresses section declares what interfaces a machine provides.
Kanvas handles conventional web rendering (HTML, CSS, React) for deployed machine surfaces. Think of it as the front door: builders work through kodex, end users walk through kanvas.
kanon
Kanon is the governance ledger. It is the append-only record of machine provenance: who created a machine, every version change, every promotion, every derivation. While the behavioral ledger records what happened during execution (runtime events), kanon records the lifecycle of machines themselves (evolution events).
Kanon and kura are separated by design: kura stores artifacts, kanon records their lineage. You can verify not just that a machine is authentic, but that its entire version history is traceable.
kits
Kits is the composable framework layer. It is a collection of approximately 60 .mashin krates for building intelligent systems. Kits is to mashin what Phoenix is to Elixir: the conventions, patterns, and reusable machinery that turn a language into a productive platform.
In the composition hierarchy: atomics (L0) are built-in step types, stdlib (L1) provides effect machines like HTTP and file access, kits (L2) provides higher-level patterns and compositions, and applications (L3) are what you build from all of these.
Kits machines live under the @kits/* namespace.
The two ledgers
mashin maintains two separate ledgers:
Behavioral Ledger: the execution flight recorder. Every machine run produces a trace: what steps ran, what decisions were made, what the LLM said, how much it cost, a hash chain proving nothing was tampered with. This is how mashin delivers runtime auditability.
Evolution Ledger: governed Git for machines. Every version change, promotion, and derivation is recorded. This is how mashin delivers lifecycle auditability. Combined with the behavioral ledger, you can answer both “what did this machine do?” and “how did this machine get here?”
The governance model
Governance in mashin is structural, not bolted on. The governance boundary and the expressiveness boundary are coterminous (the same boundary). You cannot write a machine that bypasses governance because the capability to do so does not exist in the language.
This is enforced at three levels:
- Language level:
computesteps are pure by construction (no I/O capability). All effects go through governed steps. - Runtime level: every governed step passes through the governance interpreter, which checks permissions, enforces budgets, and mediates effects.
- Kernel level: the governance interpreter is backed by kore, the formally verified kernel.
The ensures section in a machine declares what it can and cannot do. These are not annotations or comments. The runtime reads them and enforces them. See Governance for the language-level guide.
Next steps
- Quickstart - Build and run your first machine in 5 minutes
- Key Concepts - The fundamental language concepts
- Cells - Understanding the runtime environment
- koda - The intelligent development environment