Intent

Architecture as code. Verification as a build step.

Intent is a language and CLI tool for writing architectural constraints that are checked automatically – against your actual codebase with static analysis, and against state machine models with TLA+ formal verification.

The problem

Architectural decisions rot. They start as a sentence in a design doc, get restated in a code review, then slowly erode as the team grows:

"Services must not depend on storage"     → violated three PRs later
"Payment flow must reach settlement"      → nobody model-checks this
"We chose circuit breakers over retries"  → new hire adds retry logic

Linters catch style. Tests catch behavior. Nothing catches architecture – unless you make it executable.

What Intent does

You write .intent files that describe your system's structure and behavior. Intent verifies them:

1. Structural constraints are checked against your source code using static analysis (syn for Rust and regex-based analysis for TypeScript/JavaScript). These enforce layering, dependency boundaries, and module containment rules.

2. Behavioral specifications are compiled to TLA+ and model-checked with Apalache or TLC. These verify state machine properties like deadlock freedom, liveness, and safety invariants.

3. Design rationale is captured alongside constraints in a machine-readable format, producing structured decision records you can query and audit.

Quick start

cargo install intent

Write a spec (system.intent):

system PaymentPlatform {
    description "Payment processing with guaranteed settlement"

    component Processing {
        implements "crates/processing/src"
        depends_only [StorageAPI, EventQueue]

        behavior TransactionLifecycle {
            states {
                pending    { initial: true }
                processing
                settled    { terminal: true }
                failed     { terminal: true }
            }

            transitions {
                pending -> processing on receive
                processing -> settled on confirm
                processing -> failed on timeout
            }

            property eventual_settlement {
                always(pending => eventually(settled | failed))
            }
        }
    }

    constraint layering {
        !Storage.depends([API, Processing])
    }
}

Run it:

# Lint for syntax/semantic errors (no codebase needed)
intent lint system.intent

# Check structural constraints against source
intent structural system.intent --codebase src/

# Compile behaviors to TLA+ and verify with Apalache
intent compile system.intent --output out/
intent verify --obligations out/

Or run everything at once:

intent check system.intent --codebase src/

CLI commands

All commands support --format json for CI integration.

Structural constraints

Constraints are checked against your codebase using syn-based static analysis:

constraint architecture {
    // Dependency rules
    !Storage.depends([API, Domain])
    Processing.depends_only([StorageAPI, EventQueue])

    // Type reference rules
    forall s in [ServiceA, ServiceB]: s.references([AppError])

    // Trait implementation checks
    forall repo in [UserRepo, OrderRepo]: repo.implements([Repository])

    // Module containment
    API.contains([routes, handlers])
}

Built-in predicates: depends, depends_transitively, references, implements, contains – plus negated forms. Combine with forall, exists, &&, ||, =>, <=>, and !.

Behavioral specifications

State machines compile to TLA+ for formal verification:

behavior OrderSaga {
    variables {
        retries: Nat = 0
    }

    states {
        created   { initial: true }
        reserved
        charged
        completed { terminal: true }
        cancelled { terminal: true }
    }

    transitions {
        created -> reserved on reserve_inventory
        reserved -> charged on process_payment
            where { retries < 3 }
            effect { retries = retries + 1 }
        charged -> completed on confirm
        * -> cancelled on cancel
    }

    property safety {
        always(completed => !eventually(cancelled))
    }

    property liveness {
        always(created => eventually(completed | cancelled))
    }

    fairness {
        weak(reserved -> charged | cancelled)
        strong(charged -> completed | cancelled)
    }
}

Temporal operators: always, eventually, next, until, releases, weak_until, strong_releases. The transpiler targets Apalache by default; until/releases variants require TLC (--mode exhaustive).

Pattern library

Built-in patterns can be applied to behaviors without imports:

behavior OrderProcessor {
    applies EventSourced {
        subscribes: [OrderCreated, PaymentCompleted]
        emits: [ReserveInventory, ShipOrder]
    }

    applies Timeout {
        deadline: 30m
        fallback_state: "cancelled"
    }
}

Available patterns: EventSourced, Timeout, Scoped, Retry, CircuitBreaker, Saga, ProcessManager, RateLimiter, Bulkhead, CompensatingTransaction, OptimisticLocking.

Design rationale

Capture architectural decisions alongside the constraints they justify:

rationale ResilienceStrategy {
    decided because {
        "Circuit breakers fail fast, preventing cascade failures."
        "Retries cause request pileup under load."
    }
    rejected {
        retry_only: "Amplifies load during outages."
    }
    revisit when {
        "Downstream services have guaranteed response times."
    }
}

Extract as JSON with intent rationale system.intent --output decisions.json.

TLA+ expression primitives

For formal invariants, Intent supports TLA+-style expressions that transpile directly:

invariant worker_assignment {
    choose(worker, Workers, worker.status == "healthy")
}

invariant price_calculation {
    let_in { base = 100, discount = 10 } in (base - discount)
}

invariant valid_orders {
    forall order in Orders: (order.amount > 0)
}

Full set: choose, let_in, if/then/else, case, forall, exists, subset, union_all, domain_of, rec, tuple, set, fun, except, assume.

Verification modes

# Bounded model checking with Apalache (default, fast)
intent verify --obligations out/

# Exhaustive state space with TLC
intent verify --obligations out/ --mode exhaustive

# Both
intent verify --obligations out/ --mode both

# Temporal property checking (requires TLC)
intent verify --obligations out/ --temporal --mode exhaustive

Project layout

A typical project using Intent:

my-project/
  src/                    # Your Rust source code
  intent/
    system.intent         # System spec with constraints and behaviors
  out/                    # Generated TLA+ (from intent compile)

Current status

Intent is under active development. What works today:

• Structural constraint checking for Rust codebases (syn-based analysis)
• Structural constraint checking for TypeScript/JavaScript codebases (import/reference/interface checks)
• Behavioral spec compilation to TLA+ with Apalache/TLC verification
• Comprehensive linter (21 rules covering syntax, semantics, style, and dead code)
• Pattern application from the built-in standard library
• Design rationale extraction
• Hindley-Milner type inference for pattern parameters

Not yet implemented in the CLI:

• Remote pattern imports (import pattern X from "github.com/..." parses but does not resolve)
• Built-in distillation engine (the distilled keyword is parsed for forward compatibility)

Distillation – extracting Intent specs from existing codebases – is available as an external tool: intent-distill. It analyzes source code to identify architectural patterns, dependency constraints, and behavioral state machines, then generates .intent files validated with intent lint.

See LANGUAGE.md for the full language specification and DESIGN.md for architecture decisions.

License

Licensed under either of:

• Apache License, Version 2.0 (LICENSE-APACHE or http://www.apache.org/licenses/LICENSE-2.0)
• MIT license (LICENSE-MIT or http://opensource.org/licenses/MIT)

at your option.