Linear resource programming for distributed verifiable computation.
This project is at an exterimental stage and changing rapidly.
Causality is built on linear resource programming: every resource is consumed exactly once, creating explicit causal ordering and eliminating many error classes (double-spends, use-after-free, race conditions) by design. Resources are content-addressed through cryptographic hashing, enabling global deduplication, verifiable references, and natural distribution.
The system employs a three-layer architecture where each layer has precise categorical foundations:
Layer 0: Register Machine - Minimal execution substrate with 5 fundamental instructions (transform, alloc, consume, compose, tensor) based on symmetric monoidal closed category theory, operating on a linear resource heap. Designed for deterministic execution and ZK proof generation.
Layer 1: Linear Lambda Calculus - Pure functional programming with 11 primitives implementing Symmetric Monoidal Closed Category semantics. Provides unit types, tensor products, sum types, linear functions, and resource management. All operations compile to fixed-size ZK circuits.
Layer 2: Effect Algebra - Declarative programming through algebraic effects with capability-based access control. Effects separate interface from implementation, enabling cross-domain interoperability. Includes comprehensive record operations, object linearity, and intent-based orchestration.
Linear & Immutable: Resources consumed exactly once, transformations create new instances, ensuring predictable state updates and resource safety.
Self-describing: Data, code, and effects treated uniformly as content-addressed resources, enabling consistent composition through algebraic effects and verifiable global state.
Verifiable: Static analysis ensures type safety while runtime privacy and integrity maintained through efficient zero-knowledge verification.
Declarative & Composable: Algebraic effects decouple interface from implementation, enabling cross-domain interoperability through direct-style effect composition.
Resources are content-addressed entities identified by the SSZ hash of their canonical representation. A Resource binds:
- Identity: Content hash serving as global identifier
- Value: SSZ-serialized data with deterministic encoding
- Logic: Optional validation expressions for verification
- Capabilities: Access control tokens for field-level permissions
- Domains: Execution contexts enabling cross-domain operations
This unified model creates a recursive "code-as-data" architecture where resources can represent data, effects, handlers, capabilities, and system operations themselves.
Effects are pure data structures describing operations to be performed, separate from their implementation. This separation enables:
- Composability: Effects form a monad with well-defined composition laws
- Polymorphism: Same effect interface handled differently across domains
- Testability: Effects can be mocked or simulated for testing
- Verifiability: Effect execution produces verifiable traces
Capability-based access control ensures fine-grained, unforgeable permissions over resources and their fields, with capabilities forming an algebraic structure supporting intersection, union, and implication operations.
The entire architecture is designed ZK-first:
- Static Structure: All data layouts determined at compile time
- Fixed Circuits: Compilation produces bounded, deterministic circuits
- Content Addressing: Enables efficient proof verification and composition
- SSZ Merkleization: Natural tree structure for selective disclosure
Causality Lisp: Functional language with 11 core primitives mapping directly to Layer 1 operations. Supports linear types, row polymorphism, and capability annotations.
Rust DSL: Native Rust integration through traits and macros for effect definition and handler implementation.
OCaml DSL: Functional DSL leveraging OCaml's type system for constructing well-formed expressions with S-expression interop.
causality-core: Layer 0 register machine, Layer 1 linear type system, content addressingcausality-compiler: Three-layer compilation pipeline from Lisp to register instructionscausality-lisp: Linear lambda calculus interpreter with capability trackingcausality-runtime: Resource lifecycle management and effect executioncausality-simulation: Branching simulation engine with time-travel and optimizationcausality-zk: Zero-knowledge proof generation from execution tracescausality-api: Integration traits for external systems and domainscausality-toolkit: Standard library of effects, resources, and utilities
Uses Nix with Flakes for reproducible development. Enter with nix develop, build with cargo build --all, test with cargo test --all.