Project Overview

Aura is a fully peer-to-peer, private communication system that operates without dedicated servers. It uses a web-of-trust architecture to provide discovery, data availability, account recovery, and graceful async protocol evolution.

To accomplish this, Aura uses threshold cryptography so no single device holds complete keys. Network topology reflects social relationships, forming a web of trust that provides discovery, availability, and recovery. State converges through CRDT journals without central coordination. Session-typed choreographic protocols ensure safe multi-party execution.

How Aura Works

In Aura, all actors are authorities. An authority is an opaque cryptographic actor that may represent a person, a device group, or a shared context. External observers see only public keys and signed operations. This enables unlinkable participation across contexts.

State is append-only facts in journals. Each authority maintains its own journal. Shared contexts have journals written by multiple participants. Facts accumulate through CRDT merge and views are derived by reduction.

Side effects flow through explicit traits. Cryptography, storage, networking, and time are accessed only through effect handlers. This enables deterministic simulation and cross-platform portability.

Multi-party coordination uses session-typed choreographies. A global protocol specifies message flow. Each party's local behavior is projected from the global view.

Authorization passes through a layered guard chain. Before any message leaves, capabilities are verified, flow budgets are charged, and facts are committed atomically.

Aura separates key generation from agreement. Fast paths provide immediate usability while durable shared state is always consensus-finalized.

For the complete architecture, see System Architecture.

Documentation Index

The documents below cover theory, technical components, implementation guidance, and project organization.

1. Foundation

Theoretical Model establishes the formal calculus, algebraic types, and semilattice semantics underlying the system.

System Architecture describes the 8-layer architecture, effect patterns, and choreographic protocol structure.

Privacy and Information Flow Contract specifies consent-based privacy with trust boundaries, flow budgets, and leakage tracking.

Distributed Systems Contract defines safety and liveness guarantees, synchrony assumptions, and adversarial tolerance.

2. Core Systems

Cryptography documents primitives, key derivation, threshold signatures, and VSS schemes.

Identifiers and Boundaries defines the identifier types and their privacy-preserving properties.

Authority and Identity describes opaque authorities, commitment trees, and relational context structure.

Journal specifies fact-based journals, validation rules, and deterministic reduction flows.

Authorization covers capability semantics, Biscuit token integration, and guard chain authorization.

Effect System documents effect traits, handler design, and context propagation.

Runtime describes lifecycle management, guard chain execution, and service composition.

Consensus specifies single-shot agreement for non-monotone operations with witness attestation.

Operation Categories defines A/B/C operation tiers, K1/K2/K3 key generation, and agreement levels.

MPST and Choreography covers multi-party session types and choreographic protocol projection.

Transport and Information Flow specifies guard chain enforcement, secure channels, and flow receipts.

Aura Messaging Protocol (AMP) documents reliable async messaging with acknowledgment and ordering patterns.

Rendezvous Architecture covers context-scoped peer discovery and encrypted envelope exchange.

Relational Contexts specifies guardian bindings, recovery grants, and cross-authority journals.

Database Architecture defines the query layer using journals, Biscuit predicates, and CRDT views.

Social Architecture describes the three-tier model of messages, homes, and neighborhoods.

Distributed Maintenance Architecture covers snapshots, garbage collection, and system evolution.

CLI and Terminal User Interface specifies command-line and TUI interfaces for Aura operations.

Test Infrastructure Reference documents test fixtures, mock handlers, and scenario builders.

Simulation Infrastructure Reference covers deterministic simulation with virtual time and fault injection.

Formal Verification Reference describes Quint model checking and Lean theorem proving integration.

3. Developer Guides

Getting Started Guide provides a starting point for developers new to the codebase.

Effects and Handlers Guide covers the algebraic effect system, handler implementation, and platform support.

Choreography Development Guide explains choreographic protocol design, CRDTs, and distributed coordination.

Testing Guide covers test patterns, fixtures, conformance testing, and runtime harness.

Simulation Guide explains deterministic simulation for debugging and property verification.

Verification Guide documents Quint model checking and Lean proof workflows.

System Internals Guide covers guard chain internals, service patterns, and reactive scheduling.

Distributed Maintenance Guide covers operational concerns including snapshots and system upgrades.

4. Project Meta

UX Flow Coverage Report tracks harness and scenario coverage for user-visible flows.

Verification Coverage Report tracks formal verification status across Quint specs and Lean proofs.

Project Structure documents the 8-layer crate architecture and dependency relationships.