SpineDescribe the structure.
Define the rules.
The compiler does the rest.
Spine is a language for modeling systems — what exists, what can change, and what must always be true — then compiling those descriptions to verified native code.
Start Here
Evaluating practical fit
Start with the use cases if you want to see how Spine fits existing teams, procurement, migrations, and compliance workflows.
Understanding the language
Read the 16-part article series if you want the design story from facts and effects through verification and compilation.
Assessing the long-term model
Read the governance documents if you care about ecosystem boundaries, public standards, and anti-capture structure.
The problem
Software today struggles to model the real world:
- Business rules live in documents, not code
- Constraints are enforced by discipline, not by the language
- Verification is an afterthought
- State changes are hidden inside functions, invisible to analysis
Spine is designed to fix this at the language level.
What makes Spine different
Precise Types
Types that express real constraints — not just "integer" or "string", but "a list of exactly n elements" or "an asset with exactly one owner." Powered by HoTT-inspired foundations.
First-Class Reality Modeling
Facts, processes, spatial structure, and probabilistic dimensions — not bolted on, built in.
Explicit State Changes
Every action declares what must be true before it can happen, and what will be true afterward. No hidden mutations, no implicit side effects.
Verification as a Pipeline
Z3 for constraint solving, with TLA+ and mCRL2 artifact generation, and BigraphER and PRISM support planned — verification integrated into compilation, not bolted on afterward.
Universes as Context
Programs operate within structured contexts — jurisdictions, organizations, physical locations — that determine what rules apply.
Bidirectional Compilation
The compiler uses FLP correspondence relations — bidirectional mappings between Spine and Zig — so every compilation step can be reversed and verified. The self-hosting compiler compiles all 145 modules through this pipeline.
How it works
Spine programs are compiled through a verified pipeline:
Status
Spine is in active development. The compiler pipeline — surface syntax, validated IR, FLP correspondence relations, Zig backend — is taking shape. Categorical IR foundations are the design target.
Follow the technical journey on the article series, or read about how Spine changes AI-assisted coding.