菜单
Distributed systems patterns including consistency models, consensus, and fault tolerance. Load when designing or debugging distributed architectures.
用 Codex 或 Claude 帮你安装 复制这段 Prompt，粘贴到 Codex、Claude 或其他助手里，让它检查 Skill 页面并帮你完成安装。
| name | preferences-distributed-systems |
| description | Distributed systems patterns including consistency models, consensus, and fault tolerance. Load when designing or debugging distributed architectures. |
Distributed systems require explicit tradeoff decisions at architectural boundaries. This document provides a language-agnostic decision framework mapping theoretical foundations (CAP theorem, PACELC, linearizability) to practical architectural choices.
Topics covered:
For local concurrency primitives, see rust-development/11-concurrency.md. For Rust-specific distributed systems implementations, see rust-development/12-distributed-systems.md. For aggregates as local consistency boundaries, see domain-modeling.md. For effect isolation patterns, see architectural-patterns.md.
In the presence of network partitions (P), you must choose between consistency (C) and availability (A).
Consistency: All nodes see the same data at the same time. Availability: Every request receives a response (success or failure). Partition tolerance: System continues operating despite network failures.
Since network partitions are inevitable in distributed systems, the real choice is CA during normal operation, then CP or AP during partitions.
CP systems (Consistency over Availability):
AP systems (Availability over Consistency):
PACELC extends CAP by considering tradeoffs during normal operation (no partition):
If Partition: Choose Availability or Consistency (CAP) Else: Choose Latency or Consistency
During normal operation, you still face consistency vs. latency tradeoffs:
PC/EL (Partition-Consistency, Else-Latency):
PC/EC (Partition-Consistency, Else-Consistency):
PA/EL (Partition-Availability, Else-Latency):
PA/EC (Partition-Availability, Else-Consistency):
Linearizability is the strongest single-object consistency model.
Definition: Operations appear to occur instantaneously at some point between their invocation and completion, and all operations observe a single, total order.
Characteristics:
Cost: Requires coordination, reduces availability, increases latency.
When required:
When not required:
Guarantees:
Sacrifices:
When appropriate:
Implementation patterns:
Guarantees:
Sacrifices:
When appropriate:
Implementation patterns:
Conflict resolution strategies:
Guarantees:
Sacrifices:
When appropriate:
Implementation patterns:
Causality examples:
Causally related:
- User posts message (A)
- User edits message (B)
- B causally depends on A (must see edit after original)
Not causally related (concurrent):
- User Alice posts message (A)
- User Bob posts different message (B)
- A and B are concurrent (order doesn't matter)
| Requirement | Strong Consistency | Causal Consistency | Eventual Consistency |
|---|---|---|---|
| Correctness requires exact ordering | Required | Insufficient | Insufficient |
| Causality must be preserved | Sufficient | Required | Insufficient |
| High availability during partitions | Impossible | Possible | Guaranteed |
| Low latency reads/writes | Impossible | Possible | Guaranteed |
| Simple programming model | Yes (always fresh) | Moderate | No (handle staleness) |
| Financial transactions | Required | Insufficient | Insufficient |
| Collaborative editing | Overkill | Ideal | Possible (CRDTs) |
| Content delivery | Overkill | Overkill | Ideal |
Conflict-free Replicated Data Types (CRDTs) achieve eventual consistency through algebraic properties. Understanding the underlying algebraic structures clarifies when and how to use each CRDT type.
State-based CRDTs (CvRDTs) form join-semilattices: partially ordered sets where any two elements have a least upper bound (join).
Properties required:
join(join(a, b), c) = join(a, join(b, c))join(a, b) = join(b, a)join(a, a) = aThese properties ensure:
| CRDT | Algebraic Structure | Operation |
|---|---|---|
| G-Counter | Commutative monoid | Pointwise max of version vectors |
| PN-Counter | Abelian group (over integers) | Increment/decrement pairs |
| G-Set | Join-semilattice | Set union |
| 2P-Set | Pair of G-Sets | Add-set ∪, Remove-set ∪ |
| LWW-Register | Bounded join-semilattice | Max by timestamp |
| OR-Set | Complex semilattice | Tagged elements with tombstones |
The G-Counter (grow-only counter) demonstrates the monoid pattern:
use std::collections::HashMap;
#[derive(Debug, Clone)]
struct GCounter {
counts: HashMap<NodeId, u64>,
}
type NodeId = String;
impl GCounter {
// Monoid identity
fn zero() -> Self {
GCounter {
counts: HashMap::new()
}
}
// Monoid operation (commutative, associative, idempotent)
fn merge(&self, other: &GCounter) -> GCounter {
let mut result = self.counts.clone();
for (node, count) in &other.counts {
let entry = result.entry(node.clone()).or_insert(0);
*entry = (*entry).max(*count);
}
GCounter { counts: result }
}
fn value(&self) -> u64 {
self.counts.values().sum()
}
}
Op-based CRDTs (CmRDTs) require operations to be commutative. The algebraic requirement shifts from state merge to operation application.
See preferences-theoretical-foundations for the foundational laws these structures must satisfy (monoid axioms, semilattice properties, and free algebraic constructions).
Reactive streams provide backpressure-aware communication between distributed components. The stream abstraction composes algebraically while handling practical concerns like flow control.
Streams form a compositional algebra with three core components:
Source[A] → Flow[A, B] → Flow[B, C] → Sink[C]
These compose via connection operators, building complex pipelines from simple stages.
Backpressure prevents fast producers from overwhelming slow consumers. The algebraic model includes demand signaling flowing opposite to data.
Data: Source ──────────────────→ Sink
Demand: Source ←────────────────── Sink
This bidirectional flow ensures:
Event-driven bounded context communication maps naturally to streams:
use futures::StreamExt;
// Domain events flow between bounded contexts
async fn process_events(event_store: EventStore, context_id: ContextId) {
let events: impl Stream<Item = DomainEvent> =
event_store.subscribe(context_id);
let processed = events
.filter(|e| matches!(e, DomainEvent::OrderPlaced { .. }))
.map(|e| transform_to_downstream_context(e))
.ready_chunks(100); // Buffer with backpressure
downstream_context.consume(processed).await;
}
If individual stream stages preserve certain properties (e.g., ordering, exactly-once), composition preserves them. This enables reasoning about end-to-end guarantees from stage-level properties.
See event-sourcing.md for how event streams integrate with event-sourced aggregates.
Every distributed system must answer: Who owns the current state?
Three architectural positions with different tradeoffs.
The Decider pattern separates write authority from read authority through its algebraic structure.
The decide function is write authority: it validates commands against current state and produces events representing state changes.
This function embodies the business rules that determine what transitions are valid.
The evolve function is read authority: it reconstructs state from the event log by applying events sequentially.
This function represents the definitive interpretation of what each event means for the current state.
The event log is the system of record in Decider-based architectures.
State is always derivable by folding evolve over the event sequence: fold(evolve, initialState, events).
This separation enables distributed replay: any node can reconstruct state by consuming the event log, making the system resilient to failures and enabling temporal queries.
The functional purity of decide and evolve enables better testing (pure functions with no side effects) and deployment flexibility (deterministic replay on any node).
See rust-development/12-distributed-systems.md for Rust implementation patterns combining Decider with distributed event logs.
Pattern: Event sourcing with derived state.
State is computed by replaying events from authoritative log. Services derive views by consuming events. The log is the system of record.
Guarantees:
Sacrifices:
When appropriate:
Implementation:
Example: Banking system where account balance is derived from transaction events.
See also: event-sourcing.md for comprehensive event sourcing patterns, preferences-theoretical-foundations, its decide-evolve-lens reference, for the algebraic foundation (free monoid of events, state as catamorphism).
Pattern: Service owns state, events are notifications.
Service maintains canonical state (database, memory). Events published after state changes to notify other services. The service's database is the system of record.
Guarantees:
Sacrifices:
When appropriate:
Implementation:
Example: User profile service maintains current user data, publishes UserUpdated events.
Pattern: Event log authoritative for recovery, service authoritative for operations.
Used by systems like Golem for durable execution.
Service maintains current state for fast queries. Event log used for recovery after failures. Both are maintained, serving different purposes.
Guarantees:
Sacrifices:
When appropriate:
Implementation:
Example: Golem's durable execution combines in-memory state for performance with event log for recovery.
| Question | Event Log Authority | Service Authority | Hybrid |
|---|---|---|---|
| Need complete audit trail? | Required | Add separately | Available |
| Need time travel / debugging? | Built-in | Not available | Replay from log |
| Low-latency queries? | Derived views | Direct | Direct |
| Durability guarantees? | Inherent | Must implement | Inherent |
| Schema evolution complexity? | High | Low | Medium |
| Implementation complexity? | Medium | Low | High |
Choosing architectural patterns involves explicit tradeoffs. This matrix shows what you sacrifice and what you gain.
| If you choose... | You sacrifice... | You gain... |
|---|---|---|
| Event sourcing | Query latency, schema simplicity | Complete audit trail, time travel, deterministic replay |
| CQRS | Consistency between read/write models | Independent scaling, optimized read models, simpler queries |
| Actor model | Direct function calls, debuggability | Location transparency, fault isolation, natural concurrency |
| Strong consistency | Availability during partitions, latency | Correctness guarantees, simple programming model |
| Eventual consistency | Consistency, simple programming model | High availability, low latency, partition tolerance |
| Synchronous calls | Availability (cascading failures), scalability | Immediate feedback, simpler error handling |
| Asynchronous messaging | Immediate feedback, request-response simplicity | Decoupling, failure isolation, temporal independence |
| Microservices | Latency (network hops), transactions | Independent deployment, technology diversity, team autonomy |
| Monolith | Independent deployment, team autonomy | Low latency, ACID transactions, simpler deployment |
| Saga pattern | ACID transactions, rollback simplicity | Distributed transactions, service autonomy |
| Two-phase commit | Availability, performance | ACID across services (at high cost) |
Note: The CQRS pattern separates read and write models using profunctor-like structure, where commands flow one direction (write) and queries another (read). See preferences-theoretical-foundations, its observability-as-theorem reference, for the formal profunctor interpretation.
Never sacrifice correctness for convenience:
Never assume the network is reliable:
Never hide complexity in the wrong place:
The problem: Updating state AND emitting event creates divergence risk.
Dual-write occurs when two state changes must happen together but use separate mechanisms:
Why it's almost always wrong:
Example failure scenarios:
Scenario 1: Database succeeds, event publish fails
- State updated in database
- No event published
- Other services never learn about change
- System diverges
Scenario 2: Event published, database update fails
- Event published to queue
- Database update fails/rolls back
- Other services process event for non-existent state
- System diverges
Approach: Event log is the only write target. State is derived.
Write events to append-only log. Derive all state by consuming events. No dual-write because there's only one write.
Guarantees:
Sacrifices:
Implementation:
1. Validate command against current state (derived view)
2. If valid, append event to log
3. Projection services consume events and update queryable views
4. No direct state writes
When appropriate:
Approach: Write state and event in the same database transaction.
Store event in outbox table in same transaction as state update. Separate process polls outbox and publishes events. Exactly-once event publishing via transactional writes.
Guarantees:
Sacrifices:
Implementation:
BEGIN TRANSACTION
UPDATE application_state SET ...;
INSERT INTO outbox (event_type, payload, published) VALUES (..., false);
COMMIT
-- Separate process:
1. SELECT * FROM outbox WHERE published = false
2. Publish event to message queue
3. UPDATE outbox SET published = true WHERE id = ...
4. If publish fails, retry later (at-least-once delivery)
When appropriate:
Approach: Capture database changes as events automatically.
Database transaction log is the source of truth. CDC tool (Debezium, Maxwell) streams changes as events. No application-level dual-write.
Guarantees:
Sacrifices:
Implementation:
1. Application updates database normally (single write)
2. CDC tool captures transaction log
3. Transform row changes into domain events
4. Publish transformed events to message queue
When appropriate:
| Pattern | Atomic Writes | Event Granularity | Infrastructure | Schema Evolution |
|---|---|---|---|---|
| Event log only | Inherent | Domain events | Event store | Complex |
| Transactional outbox | Yes | Domain events | Outbox processor | Medium |
| Change data capture | Yes | Low-level (rows) | CDC tool + transforms | Simple |
Recommendation: Use transactional outbox for most microservices architectures. Use event sourcing (event log only) when complete history is required. Avoid CDC unless retrofitting existing systems.
Distributed systems deliver messages at-least-once. Operations must be safe to retry. Idempotency must be designed in, not added later.
An operation is idempotent if executing it multiple times has the same effect as executing it once.
Mathematical definition: f(f(x)) = f(x)
This corresponds to monoid identity laws: applying an operation multiple times has the same effect as applying it once. See preferences-theoretical-foundations for the algebraic foundation of idempotency in distributed systems.
Examples:
At-least-once delivery: Message queues guarantee delivery but may deliver duplicates. Retry mechanisms: Failed operations are retried, potentially succeeding multiple times. Network failures: Unclear if operation succeeded when network fails mid-request.
Without idempotency:
Approach: Client provides unique key per request. Server tracks processed keys.
Client generates idempotency key (UUID, request ID). Server checks if key already processed. If yes, return cached result. If no, process request, store key with result, return result.
Guarantees:
Implementation:
1. Client: POST /payment {"amount": 100, "idempotency_key": "uuid-1234"}
2. Server:
- Check if uuid-1234 in processed_requests table
- If found: return cached result
- If not found:
BEGIN TRANSACTION
INSERT INTO processed_requests (key, result) VALUES ("uuid-1234", NULL)
result = process_payment(100)
UPDATE processed_requests SET result = result WHERE key = "uuid-1234"
COMMIT
return result
When appropriate:
Caching strategy:
Approach: Design operations to be naturally idempotent.
Operations are inherently safe to retry without explicit deduplication.
Examples:
Idempotent by nature:
- SET status = "COMPLETED"
- DELETE record WHERE id = 123
- PUT /resource/123 {"name": "Alice"}
- Add item to set (sets ignore duplicates)
Not naturally idempotent:
- INCREMENT counter
- APPEND to list
- POST /resource (creates new resource each time)
When appropriate:
Approach: Operations check preconditions and succeed only once.
Use version numbers, timestamps, or state checks to ensure single application.
Examples:
Version-based:
UPDATE account SET balance = 100 WHERE id = 123 AND version = 5
State-based:
UPDATE order SET status = "SHIPPED" WHERE id = 123 AND status = "PENDING"
(only succeeds if status is PENDING, retries are no-ops)
Timestamp-based:
INSERT INTO events (id, timestamp) VALUES (123, "2025-01-01")
(unique constraint on id prevents duplicates)
Guarantees:
When appropriate:
When composing multiple services, idempotency must compose:
Anti-pattern:
Service A (idempotent) calls Service B (not idempotent)
- Retry in A causes duplicate call to B
- B processes duplicate
- System diverges
Pattern:
Service A generates idempotency key, passes to Service B
- Service A: POST /process {"key": "uuid-1234", ...}
- Service B: checks key, processes once
- Retry in A sends same key to B
- Service B returns cached result
- End-to-end idempotency
Recommendation: Require idempotency keys in all inter-service APIs with side effects.
Sagas coordinate distributed transactions across multiple services without requiring distributed locks or two-phase commit.
A saga is a sequence of local transactions where each service updates its own data and publishes an event or message. If any step fails, compensating transactions undo completed steps.
Key insight: Sagas are isomorphic to actors (state + messages). Each step is a message to a stateful service. Compensation is reverse message flow.
Approach: Central orchestrator service directs the saga.
Orchestrator knows all steps and their order. Orchestrator sends commands to services. Services respond with success or failure. On failure, orchestrator triggers compensating transactions.
Structure:
Orchestrator
├─> Service A: do X
├─> Service B: do Y
├─> Service C: do Z
└─> If failure: Service A: undo X, Service B: undo Y
Guarantees:
Sacrifices:
Implementation:
Orchestrator state machine:
1. Send command to Service A
2. Await response
3. If success: Send command to Service B
4. If failure: Send compensation to Service A, exit
5. Continue for all steps
6. If any step fails: walk backward sending compensations
When appropriate:
Example: Order processing saga:
1. Reserve inventory (Inventory Service)
2. Charge payment (Payment Service)
3. Ship order (Shipping Service)
4. If any step fails: reverse prior steps
Approach: Services listen for events and decide their own actions.
No central orchestrator. Each service knows what to do when certain events occur. Services publish events, other services react.
Structure:
Service A: does X, publishes EventX
Service B: listens for EventX, does Y, publishes EventY
Service C: listens for EventY, does Z
Service B: listens for FailureZ, undoes Y, publishes CompensationY
Service A: listens for CompensationY, undoes X
Guarantees:
Sacrifices:
Implementation:
Service A:
on PlaceOrderCommand:
reserve_inventory()
publish InventoryReserved
Service B:
on InventoryReserved:
charge_payment()
publish PaymentCharged
Service C:
on PaymentCharged:
ship_order()
publish OrderShipped
Service B:
on ShippingFailed:
refund_payment()
publish PaymentRefunded
Service A:
on PaymentRefunded:
release_inventory()
publish InventoryReleased
When appropriate:
Example: User signup saga:
UserService: creates user, publishes UserCreated
EmailService: sends welcome email
NotificationService: sends push notification
(No compensation needed, all steps eventually succeed)
Compensating transactions undo the effects of completed transactions.
Not true rollback: Original transaction is committed. Compensation creates new transaction to reverse effects.
Semantic compensation: Compensation must make semantic sense (not just database rollback).
Examples:
Transaction: Reserve inventory (decrement stock count)
Compensation: Release inventory (increment stock count)
Transaction: Charge credit card
Compensation: Refund credit card
Transaction: Send email
Compensation: Send cancellation email (cannot unsend original)
Design guidelines:
Partial compensation:
Some transactions cannot be fully compensated. Use best-effort compensation and notify users.
Example: Cannot cancel shipped order. Compensation: Issue refund, arrange return pickup, notify user.
| Criteria | Orchestration | Choreography |
|---|---|---|
| Complex logic | Better | Worse |
| Service coupling | High | Low |
| Observability | Easy (central view) | Hard (distributed trace) |
| Single point of failure | Yes (orchestrator) | No |
| Evolution | Hard (orchestrator changes) | Easy (services independent) |
| Debugging | Easy (state machine) | Hard (event flow) |
Recommendation: Use orchestration for complex sagas requiring control flow. Use choreography for simple event-driven workflows.
Deterministic replay rebuilds system state by re-executing operations from a log. Critical for durability, debugging, and compliance.
Theoretical foundation: State reconstruction from event log is a catamorphism (fold) over the event sequence. See preferences-theoretical-foundations, its decide-evolve-lens reference, for the category-theoretic interpretation of event replay as structural recursion.
Durability guarantees:
Debugging and auditing:
Compliance requirements:
No non-deterministic operations in replay path:
Operations must produce the same result when replayed.
Forbidden:
Allowed:
Example:
Bad (non-deterministic):
let order_id = generate_random_uuid() // Different each replay
let timestamp = now() // Different each replay
Good (deterministic):
let order_id = event.order_id // Captured in event
let timestamp = event.timestamp // Captured in event
Strict operation ordering:
Operations must be totally ordered. Concurrent operations are not deterministic during replay.
Solution: Assign sequence numbers or timestamps to establish total order.
Snapshot + event replay hybrid:
Full replay from beginning is expensive. Use snapshots to reduce replay time.
Pattern:
1. Take snapshot of state at time T
2. Store snapshot
3. Replay events from time T to present
4. Reconstruct current state
Guarantees:
Tradeoffs:
Event sourcing: Events are the source of truth, state derived.
1. Append event to log
2. Replay events from log to rebuild state
3. Snapshot state periodically
4. Replay only events since last snapshot
Actor persistence (Akka, Orleans):
1. Actor processes command
2. Persist event to journal
3. Update in-memory state
4. On recovery: replay events from journal
Database write-ahead log (WAL):
1. Write operation to WAL before applying to database
2. On crash: replay WAL to restore state
3. Checkpoint periodically to truncate WAL
Capture external inputs:
Store responses from external systems in event log. Replay uses recorded responses, not live calls.
Example:
Original execution:
1. Call external service: response = fetch_price(product_id)
2. Store event: PriceFetched(product_id, response)
Replay:
1. Read event: PriceFetched(product_id, response)
2. Use recorded response (no external call)
Handle time carefully:
Do not use now() during replay.
Store timestamps in events.
Example:
Command: PlaceOrder(items, timestamp)
timestamp: client-provided or captured at ingestion
Event: OrderPlaced(order_id, items, timestamp)
timestamp: from command (deterministic)
Random number generation:
Record random values in events.
Example:
Original execution:
1. Generate: request_id = uuid4()
2. Store event: RequestCreated(request_id)
Replay:
1. Read event: RequestCreated(request_id)
2. Use recorded request_id (no random generation)
Distributed systems patterns described in this skill each have specific observability requirements. Without targeted instrumentation, the failure modes these patterns address remain invisible until they produce user-facing incidents.
Circuit breaker state transitions from closed to open to half-open and back to closed should be emitted as metrics with labels for the target service and failure reason. The open-circuit rate across the fleet indicates systemic dependency failures. Half-open probe success and failure rates indicate recovery progress. Alert on sustained open-circuit state because it means a dependency is persistently unavailable and the circuit breaker is doing its job, but the underlying problem needs attention.
Saga and workflow observability requires that each saga step creates a span within the saga's trace. Step completion, compensation triggers, and final saga outcome (committed versus compensated) should be recorded. For choreography-based sagas, the correlation ID (trace_id) propagated through events is the only mechanism connecting steps across services. For orchestration-based sagas, the orchestrator creates the parent span and each step is a child. Compensation frequency by step identifies which steps are most fragile and likely to trigger rollback.
Retry attempts should be recorded as span events rather than separate spans to avoid inflating trace cardinality. Track retry count per operation, backoff duration distribution, and final outcome distinguishing success after N retries from retry exhaustion. High retry rates for a specific dependency indicate degradation before circuit breakers trip.
Queue and event bus observability centers on consumer lag, the difference between latest produced offset and latest consumed offset, as the primary health indicator. Track queue depth, publish rate, consume rate, and processing latency per consumer group. Dead letter queue depth indicates messages that failed processing and need investigation, not just counting. For event-sourced systems, projection lag measuring the time between event persistence and projection update indicates read-model freshness.
Idempotency key collision rate distinguishes retries, which are expected, from duplicate submissions, which indicate potential client bugs. Track collision rate by endpoint and client to identify problematic callers.
Outbox drain lag, measuring the time between row insertion and successful publish, indicates the reliability of the outbox relay. A growing outbox table size suggests the relay is falling behind or failing. Monitor both the outbox processor's poll frequency and its success rate to distinguish between a processor that is not running and one that is running but encountering failures.
Network partition detection manifests as simultaneous connection failures to a subset of nodes. Correlated timeout spikes across multiple services talking to the same dependency cluster suggest a partition. This requires cross-service trace analysis because single-service metrics are insufficient to distinguish a partition from a single-node failure. Distributed tracing with consistent trace_id propagation across all services is the prerequisite for this kind of analysis.
The observability requirements of these patterns compose: a saga step that includes a circuit-breaker-protected call with retry logic should produce a saga step span containing retry span events, with circuit breaker metrics emitted independently. Each layer of resilience pattern adds its own observability without interfering with the others.
Cross-reference preferences-observability-engineering for the general observability model, preferences-event-sourcing for event store-specific observability, and preferences-production-readiness for operational practices.
Use this checklist before implementing distributed system features.
Question: Who owns the current state?
Rationale: [Explain why this authority model fits your requirements]
Tradeoffs accepted: [What are you sacrificing with this choice?]
Question: What consistency guarantees are required?
Rationale: [Why this consistency model?]
CAP choice: During partitions, favor:
PACELC choice: During normal operation, favor:
Question: How do you avoid dual-write problems?
Implementation: [Describe how state and events remain consistent]
Question: How are operations made idempotent?
Cross-service propagation: [How do idempotency keys flow across services?]
Question: How are failures and partial failures handled?
Distributed transactions:
Compensation: [Describe compensating transactions for each step]
Retry logic:
Timeouts: [Specify timeout values and backoff strategies]
Question: Must the system support deterministic replay?
If yes:
now())Question: How will you debug distributed operations?
Correlation strategy: [How are requests correlated across services?]
Feature: Order processing system
1. Authority model: Service as authority (transactional outbox)
2. Consistency model: Strong consistency within order service, eventual across services
3. Dual-write avoidance: Transactional outbox
4. Idempotency: Idempotency keys on all APIs
idempotency_key headerprocessed_requests table (24h TTL)5. Failure handling: Orchestrated saga pattern
6. Deterministic replay: Not required (no compliance needs)
7. Observability: OpenTelemetry with trace IDs
event-sourcing.md (comprehensive event sourcing patterns, process managers, CQRS)rust-development/11-concurrency.md (local concurrency primitives)rust-development/12-distributed-systems.md (Rust-specific distributed implementations)domain-modeling.md (aggregates as consistency boundaries)architectural-patterns.md (effect isolation, onion architecture)railway-oriented-programming.md (Result types for distributed error handling)hypermedia-development/07-event-architecture.md (SSE streaming as event projection, CQRS in hypermedia context)Index curated reference corpora into a searchable knowledge graph via the cognee engine, then query it to ground technical writing, review, and analysis. Use when ingesting reference documents into named datasets or retrieving grounding context for tasks like drafting or reviewing a manuscript. A reference-knowledge index, explicitly not agent session memory.
Nix development conventions for flakes, derivations, modules, and code style. Use when authoring flake.nix files, writing derivations or builders, designing NixOS/nix-darwin/home-manager modules, or following nix formatting and naming conventions. For check architecture and CI integration, see preferences-nix-checks-architecture and preferences-nix-ci-cd-integration.
Approximately-verifiable, refinement-driven development for type-driven domain-driven design. Use when modeling a domain as a dependently-typed Lean 4 specification, refining/lowering it to a Rust implementation, lifting the implementation back via Charon and Aeneas to check spec<->implementation correspondence (translation validation) — mechanically when tractable, otherwise via differential testing or LLM comparison — or when generating and diffing type-system diagrams of the model and implementation to track their evolution. Mechanical on-the-nose proof is the precise ideal, not a requirement; its absence is not a failure of the method.
Guide for creating effective skills. This skill should be used when users want to create a new skill (or update an existing skill) that extends Claude's capabilities with specialized knowledge, workflows, or tool integrations.
Algebraic data type patterns including sum types, product types, and pattern matching across languages. Load when designing type hierarchies or working with discriminated unions.
Algebraic laws including functor/monad laws and property-based testing strategies. Load when verifying algebraic properties or writing property tests.