IntentLang

IntentLang is a declarative specification language for human-AI collaboration.

Humans write what the system must do and what constraints must hold. Agents handle how — generating verifiable implementations from specs. The toolchain proves the implementation satisfies the contract.

From vibe coding to agentic engineering

Vibe coding proved something important: you can describe what you want in plain language and an AI will generate code for it. But it also exposed a gap — without formal contracts, you're left eyeballing the output and hoping it works.

IntentLang closes that gap. It keeps the natural language starting point that makes vibe coding accessible, then adds the structure that makes the result trustworthy: formal specs, machine-checked contracts, and an audit trail that traces every line of generated code back to a requirement.

The shift is simple: instead of prompting and praying, you specify and verify.

How it works

IntentLang addresses this with four layers:

0. Natural Language — Describe what you want in plain English. An AI agent generates a formal spec from your description. The lowest-barrier entry point.
1. Intent Layer — Write or refine declarative specs directly: entities, actions, pre/postconditions, invariants. Readable by anyone on the team, formally parseable by machines.
2. Agent IR — Agents generate a dense, typed intermediate representation from specs. Optimized for machine generation, not human authoring.
3. Audit Bridge — Tooling maps every IR construct back to a spec requirement. Orphan code (implementation without spec justification) is a first-class error.

Layers 0 and 1 are both human-facing — the system meets you where you are.

Quick Example

module TransferFunds

--- A fund transfer between two accounts within the same currency.

entity Account {
  id: UUID
  balance: Decimal(precision: 2)
  currency: CurrencyCode
  status: Active | Frozen | Closed
}

action Transfer {
  from: Account
  to: Account
  amount: Decimal(precision: 2)

  requires {
    from.status == Active
    to.status == Active
    from.currency == to.currency
    amount > 0
    from.balance >= amount
  }

  ensures {
    from.balance == old(from.balance) - amount
    to.balance == old(to.balance) + amount
  }
}

invariant NoNegativeBalances {
  forall a: Account => a.balance >= 0
}

$ intent check examples/transfer.intent
OK: TransferFunds — 7 top-level item(s), no issues found

Prior Art

IntentLang draws on Design by Contract (requires/ensures), Dafny (verification-aware programming), TLA+ (system-level invariants), and Alloy (lightweight formal modeling).

Installation

From crates.io

If you have Rust installed:

cargo install intent-cli

This installs the intent binary to ~/.cargo/bin/.

Build from source

Requires Rust 1.70+.

git clone https://github.com/krakenhavoc/IntentLang.git
cd IntentLang
cargo build --release -p intent-cli
# Binary at target/release/intent

Pre-built binary (Linux x86_64)

Download from the latest release:

chmod +x intent-linux-x86_64
./intent-linux-x86_64 check examples/transfer.intent

Docker

docker build -t intent .
docker run -v $(pwd)/examples:/work intent check /work/transfer.intent

Verify installation

intent --help

You should see the list of available subcommands: check, render, render-html, compile, verify, audit, coverage.

Your First Spec

Let's write a simple IntentLang spec from scratch and run it through the toolchain.

Create a file

Create hello.intent with the following content:

module HelloWorld

--- A minimal task tracker to demonstrate IntentLang basics.

entity Task {
  id: UUID
  title: String
  done: Bool
}

action CompleteTask {
  task: Task

  requires {
    task.done == false
  }

  ensures {
    task.done == true
  }
}

invariant TasksHaveTitle {
  forall t: Task => t.title != ""
}

Check it

Run the semantic checker:

intent check hello.intent

Output:

OK: HelloWorld — 3 top-level item(s), no issues found

The checker validates:

• All types are defined or built-in
• Field accesses are valid
• old() is only used in ensures blocks
• Quantifier bindings reference valid types
• No tautological comparisons

Render it

Generate a Markdown summary:

intent render hello.intent

Or a self-contained HTML document:

intent render-html hello.intent > hello.html

Compile to IR

Lower the spec to Agent IR:

intent compile hello.intent

This outputs a JSON representation of the typed intermediate representation that agents can consume.

Verify

Run structural verification on the compiled IR:

intent verify hello.intent

This checks that the IR is well-formed, all references resolve, and coherence obligations are satisfied.

What's next?

• Read the Language Reference for the full syntax
• Browse the Examples to see real-world specs
• See the CLI Reference for all available commands

Modules

Every .intent file begins with a module declaration:

module TransferFunds

The module name must start with an uppercase letter and use PascalCase. It serves as a namespace for all definitions in the file.

Documentation blocks

Documentation blocks use --- and can appear after the module declaration or before any entity, action, or invariant:

module TransferFunds

--- A fund transfer system between accounts within the same currency.
--- Supports basic account-to-account transfers with balance validation,
--- idempotency guarantees, and manager approval for large amounts.

Documentation blocks are preserved in rendered output and audit traces, making them useful for explaining design intent to both humans and tooling.

Imports

Modules can import definitions from other modules using use declarations. Imports appear after the doc block and before any top-level items.

Whole-module import

Import all entities, actions, and invariants from another module:

module Banking

use Types

This makes every definition from the Types module available in Banking. The resolver looks for Types.intent in the same directory as the importing file.

Selective import

Import a single item from another module:

module Banking

use Types.Account

This imports only the Account entity from Types.

Multiple imports

module App

use Types
use Auth.User
use Billing

Resolution rules

• use Foo looks for Foo.intent in the same directory as the importing file.
• Circular imports are detected and produce an error.
• Diamond dependencies (A imports B and C, both import D) are handled correctly -- each module is parsed only once.
• Imported definitions do not shadow local definitions. If both the local module and an imported module define Account, the local definition takes precedence.

Example: multi-module project

Types.intent:

module Types

entity Account {
  id: UUID
  balance: Decimal(precision: 2)
  status: Active | Frozen | Closed
}

Banking.intent:

module Banking

use Types

action Transfer {
  from: Account
  to: Account
  amount: Decimal(precision: 2)

  requires {
    from.status == Active
    to.status == Active
    amount > 0
    from.balance >= amount
  }

  ensures {
    from.balance == old(from.balance) - amount
    to.balance == old(to.balance) + amount
  }
}

$ intent check Banking.intent
OK: Banking — 1 top-level item(s), no issues found

Entities

Entities define data structures with typed fields:

entity Account {
  id: UUID
  owner: String
  balance: Decimal(precision: 2)
  currency: CurrencyCode
  status: Active | Frozen | Closed
  created_at: DateTime
}

Fields

Each field has a name and a type, separated by :. Field names use snake_case.

Fields can use any of the available types:

entity CartItem {
  product: Product       // reference to another entity
  quantity: Int          // primitive type
  notes: String?         // optional type
  tags: List<String>     // collection type
}

Documentation

Entities can have documentation blocks:

entity TransferRecord {
  --- Records a completed or pending transfer for audit purposes.
  id: UUID
  amount: Decimal(precision: 2)
  status: Pending | Completed | Failed | Reversed
}

Entity references

Entities can reference other entities as field types. The checker validates that all referenced entity names are defined:

entity Order {
  id: UUID
  cart: Cart           // must be defined as an entity
  total: Decimal(precision: 2)
}

If Cart is not defined, the checker reports:

intent::check::undefined_type

  × undefined type `Cart`
  help: define an entity named `Cart`, or use a built-in type

Actions

Actions define operations with parameters, preconditions, postconditions, and properties:

action Transfer {
  from: Account
  to: Account
  amount: Decimal(precision: 2)

  requires {
    from.status == Active
    to.status == Active
    from.currency == to.currency
    amount > 0
    from.balance >= amount
  }

  ensures {
    from.balance == old(from.balance) - amount
    to.balance == old(to.balance) + amount
  }

  properties {
    idempotent: true
    atomic: true
    audit_logged: true
  }
}

Parameters

Action parameters are listed at the top of the block, before any requires, ensures, or properties sections. Each parameter has a name and type.

Requires (preconditions)

The requires block lists conditions that must be true before the action executes. Each line is a boolean expression. If any precondition is false, the action must not execute.

old() cannot be used in requires blocks — preconditions describe the current state, not a state transition.

Ensures (postconditions)

The ensures block lists conditions that must be true after the action executes. Use old(expr) to reference the value of an expression before the action ran:

ensures {
  from.balance == old(from.balance) - amount
  to.balance == old(to.balance) + amount
}

Properties

The properties block contains key-value metadata about the action. Properties are not validated semantically — they're metadata for downstream tooling:

properties {
  idempotent: true
  idempotency_key: request_id
  atomic: true
  audit_logged: true
  max_latency_ms: 500
  requires_role: "compliance_officer"
}

Documentation

Actions support inline documentation:

action FreezeAccount {
  --- Freeze an account, preventing all transfers.
  account: Account
  reason: String

  requires {
    account.status == Active
  }

  ensures {
    account.status == Frozen
  }
}

Invariants

Invariants define system-wide constraints that must always hold, regardless of which action executes:

invariant NoNegativeBalances {
  --- No account may ever have a negative balance.
  forall a: Account => a.balance >= 0
}

Quantifiers

Invariants typically use quantifiers to express universal or existential properties:

// Universal: must hold for all instances
invariant StockNonNegative {
  forall p: Product => p.stock >= 0
}

// Temporal: constrains action effects
invariant TransferConservation {
  forall t: Transfer =>
    old(t.from.balance) + old(t.to.balance) ==
    t.from.balance + t.to.balance
}

When an invariant quantifies over an action type (like forall t: Transfer), it becomes a temporal invariant — a constraint on the state transition that the action produces. old() is valid in these contexts.

Verification obligations

The IR verifier automatically detects coherence obligations — situations where an action modifies fields that an invariant constrains. For example, if Transfer modifies balance and NoNegativeBalances constrains balance, the verifier flags this as an obligation that the implementation must satisfy.

intent verify examples/transfer.intent

The output includes a section listing these obligations, connecting each invariant to the actions that might affect it.

Edge Cases

The edge_cases block defines boundary conditions as pattern-matched rules:

edge_cases {
  when amount > 10000.00 => require_approval(level: "manager")
  when from.owner == to.owner => allow(note: "Self-transfer between own accounts")
  when from.currency != to.currency => reject("Cross-currency transfers not supported.")
}

Syntax

Each edge case rule follows the pattern:

when <condition> => <handler>

The condition is a boolean expression. The handler is a function call with optional named arguments.

Common handlers

These are conventions — handlers are not validated by the checker, but are meaningful to downstream tooling:

Edge case validation

The checker validates that field references in edge case conditions refer to valid fields on known entity types. Undefined fields or entities produce errors with source spans.

State Machines

State machines define named types with explicit allowed transitions between states.

Syntax

state StatusName {
  StateA -> StateB -> StateC
  StateA -> StateD
}

Each transition chain (->) declares that transitions between adjacent states are valid. Multiple chains can share states to express branching.

Example

module TaskTracker

state TaskStatus {
  Open -> InProgress -> Done
  Open -> Cancelled
  InProgress -> Blocked -> InProgress
}

entity Task {
  id: UUID
  title: String
  status: TaskStatus
}

action StartTask {
  task: Task

  requires {
    task.status == Open
  }

  ensures {
    task.status == InProgress
  }
}

This defines TaskStatus as a type with five states (Open, InProgress, Done, Cancelled, Blocked) and these valid transitions:

• Open → InProgress
• InProgress → Done
• Open → Cancelled
• InProgress → Blocked
• Blocked → InProgress

Type Registration

A state name registers as a type, just like entity. You can use it as a field type, action parameter type, or quantifier binding type.

Documentation

State machines support doc blocks:

--- Tracks the lifecycle of a customer order.
state OrderStatus {
  Pending -> Confirmed -> Shipped -> Delivered
  Pending -> Cancelled
}

Code Generation

intent codegen produces language-idiomatic enums with transition validation:

Cross-Module Imports

State machines are included when importing a module with use:

module Types

state OrderStatus {
  Pending -> Confirmed -> Shipped
}

module Main

use Types

entity Order {
  id: UUID
  status: OrderStatus
}

Type System

IntentLang has a rich type system designed for specification clarity.

Primitive types

Numeric types

balance: Decimal(precision: 2)

Decimal(precision: N) specifies a fixed-precision decimal number. The precision parameter indicates the number of decimal places.

Domain types

Domain types are extensible — they serve as semantic markers for downstream tooling.

Collection types

items: List<CartItem>       // ordered list
tags: Set<String>           // unique set
metadata: Map<String, Int>  // key-value map

Optional types

Append ? to make a type optional:

locked_until: DateTime?     // may be null
last_login: DateTime?

Union types

Union types define a closed set of possible values:

status: Active | Frozen | Closed

Union variants are enum-like labels (PascalCase). They are not references to other types — Active is a value, not a type.

Expressions

Expressions are used in requires, ensures, invariant, and edge_cases blocks.

Comparison operators

Logical operators

The implication operator => is right-associative: a => b means "if a, then b".

Quantifiers

// Universal quantifier
forall a: Account => a.balance >= 0

// Existential quantifier
exists s: Session => s.user.email == email && s.revoked == false

Quantifiers bind a variable to a type and apply a predicate. The binding type must be a defined entity or action.

Field access

from.balance
from.status
item.product.name

Dotted field access navigates entity fields. The checker validates that each field exists on the referenced type.

Function calls

old(from.balance)           // pre-state reference
now()                       // current time
lookup(User, email)         // entity lookup
password_verified(a, b)     // domain function
require_approval(level: "manager")  // with named args

old(expr)

References the value of an expression before the current action executed. Only valid in ensures blocks and temporal invariants (invariants that quantify over actions).

ensures {
  from.balance == old(from.balance) - amount
}

Using old() in a requires block is an error:

intent::check::old_in_requires

  × `old()` cannot be used in a `requires` block
  help: `old()` references pre-state values and is only meaningful in `ensures` blocks

Literals

42              // integer
10000.00        // decimal
"hello"         // string
true / false    // boolean
null            // null (for optional comparisons)

CLI Usage

The intent CLI provides commands for checking, rendering, compiling, and verifying IntentLang specs.

intent <command> <file>

Commands

Global options

intent --output json    JSON output (for agent consumption)
intent --help           Show help
intent --version        Show version

See the subpages for detailed usage of each command.

Checking Specs

intent check <file>

The check command parses a .intent file and runs six semantic analysis passes:

1. Collect definitions — gather all entity, action, and invariant names; detect duplicates
2. Resolve type references — verify that all types are either built-in or defined as entities
3. Validate quantifier bindings — ensure forall/exists bind to valid entity or action types
4. Validate edge case actions — check that edge case handlers reference valid operations
5. Validate field access — verify dotted field access on entity-typed parameters
6. Constraint validation — check old() placement and detect tautological comparisons

Success output

$ intent check examples/transfer.intent
OK: TransferFunds — 7 top-level item(s), no issues found

Error output

Errors include source spans, labels, and actionable help via miette:

intent::check::undefined_type

  × undefined type `Customer`
   ╭─[5:13]
 4 │       id: UUID
 5 │ ╭─▶   customer: Customer
 6 │ ├─▶   items: List<LineItem>
   · ╰──── used here
 7 │     }
   ╰────
  help: define an entity named `Customer`, or use a built-in type

intent::check::old_in_requires

  × `old()` cannot be used in a `requires` block
    ╭─[13:21]
 12 │       requires {
 13 │ ╭─▶     from.balance == old(from.balance)
 14 │ ├─▶   }
    · ╰──── used here
    ╰────
  help: `old()` references pre-state values and is only meaningful in `ensures` blocks

Rendering

Markdown

intent render <file>

Produces a Markdown document with:

• Module name and documentation
• Entity field tables
• Action signatures with pre/postconditions
• Invariant descriptions
• Edge case rules

Suitable for sharing with non-technical stakeholders or embedding in project documentation.

HTML

intent render-html <file> > output.html

Produces a self-contained HTML document with color-coded sections. No external CSS or JavaScript dependencies — the output is a single file you can open in any browser.

intent render-html examples/transfer.intent > transfer.html
open transfer.html

Compiling to IR

intent compile <file>

Lowers an IntentLang spec to the Agent IR — a typed intermediate representation designed for machine consumption.

The output is JSON, suitable for piping to other tools:

intent compile examples/transfer.intent > transfer.ir.json
intent compile examples/transfer.intent | jq '.entities'

What the IR contains

The Agent IR includes:

• Entities with typed fields and source traces
• Actions with lowered preconditions, postconditions, and properties
• Invariants with fully resolved expressions
• Edge case rules with condition/handler pairs

Every IR node carries a SourceTrace linking it back to the original spec location (file, line, column). This trace is the foundation of the audit bridge.

Verification & Audit

Verify

intent verify <file>

Runs structural verification and coherence analysis on the compiled IR:

• Structural checks — all type references resolve, field accesses are valid, old() appears only in valid contexts
• Coherence analysis — detects verification obligations: invariants that constrain fields modified by actions

The output lists any verification errors and the set of coherence obligations that an implementation must satisfy.

Incremental Verification

intent verify --incremental <file>

Caches per-item verification results in .intent-cache/. On subsequent runs, only re-verifies items whose content has changed. Reports how many items were re-verified vs cached.

Audit

intent audit <file>

Displays the audit trace map — a mapping from every spec-level construct to its IR representation, with source line references. This lets you verify that every spec requirement has a corresponding IR construct.

Coverage

intent coverage <file>

Shows a coverage summary: counts of entities, actions, invariants, and edge cases, along with their verification status. Useful for quick assessment of spec completeness.

Agent Tooling

Commands designed for agent integration: structured queries, spec diffing, JSON output, and multi-agent collaboration.

JSON Output

Any command supports --output json for structured, machine-readable output:

intent --output json check examples/transfer.intent
intent --output json verify examples/transfer.intent

Diff

intent diff <old-file> <new-file>

Shows a spec-level diff between two versions of a spec file. Reports added, removed, and modified spec items — useful for reviewing changes before committing or verifying that a refactor preserved all constraints.

Query

intent query <file> <target>

Query specific items from a spec. Available targets:

Combine with --output json for structured output that agents can parse directly.

Multi-Agent Collaboration

When multiple agents work on the same spec, the locking system prevents conflicts.

Lock

intent lock <file> <item> --agent <agent-id>

Claims a spec item for an agent. Other agents cannot claim the same item until it is unlocked. Lock state is stored in .intent-lock/.

Unlock

intent unlock <file> <item> --agent <agent-id>

Releases a claimed spec item. Only the agent that locked it can unlock it.

Status

intent status <file>

Shows lock status for all spec items — which items are claimed, by whom, and which are available.

Generating Specs from Natural Language (Layer 0)

The intent generate command translates plain English descriptions into validated .intent specs using an AI model.

Quick Start

# Set your API key
export AI_API_KEY=your-key-here

# Generate a spec from a description
intent generate "I want a program that greets a user by name"

# Write output to a file
intent generate --out hello.intent "a greeting service"

Modes

Single-shot (default)

Generates a spec, validates it, and outputs the result:

intent generate "a task tracker with priorities and assignments"

Interactive

Ask clarifying questions before and during generation:

intent generate --interactive "build me a shopping cart"

Edit existing spec

Modify an existing .intent file from a natural language description:

intent generate --edit cart.intent "add a discount code feature"
intent generate --edit cart.intent --diff "add rate limiting"  # show diff instead

Confidence Levels

The --confidence flag (1-5) controls how much the agent asks vs. assumes:

Configuration

Environment variables

CLI flags

How it works

1. Constructs a system prompt with IntentLang syntax reference and examples
2. Sends the user's description to the LLM via OpenAI-compatible API
3. Extracts the .intent code from the response
4. Validates via intent check (parser + semantic analysis)
5. If errors, feeds them back to the LLM for correction (up to --max-retries)
6. Outputs the validated spec

Prompt preservation

The natural language prompt used to generate a spec should be committed to version control alongside the .intent file. This preserves the original ask so team members can understand the intent behind the spec.

Serving Specs (Runtime API)

intent serve <file>

Starts a stateless HTTP server that exposes your spec's actions as REST endpoints. The runtime enforces preconditions, computes postconditions, and validates invariants on every request.

Options

Example

$ intent serve examples/transfer.intent
intent serve: listening on http://127.0.0.1:3000
  module: TransferFunds
  POST /actions/Transfer
  GET  /

Endpoints

GET / — Module info

Returns the module's entities, actions, and invariants:

{
  "name": "TransferFunds",
  "entities": [
    {
      "name": "Account",
      "fields": [
        { "name": "id", "type": "Named(\"UUID\")" },
        { "name": "balance", "type": "Decimal(2)" },
        { "name": "status", "type": "Union([\"Active\", \"Suspended\"])" }
      ]
    }
  ],
  "actions": [
    {
      "name": "Transfer",
      "params": [
        { "name": "from", "type": "Struct(\"Account\")" },
        { "name": "to", "type": "Struct(\"Account\")" },
        { "name": "amount", "type": "Decimal(2)" }
      ],
      "precondition_count": 4,
      "postcondition_count": 2
    }
  ],
  "invariants": ["BalanceNonNegative"]
}

POST /actions/<name> — Execute an action

Executes the named action against caller-provided state. The server is stateless — you provide all entity state in each request and receive the new state in the response.

Request format

{
  "params": {
    "from": { "id": "1", "balance": 1000.0, "status": "Active" },
    "to": { "id": "2", "balance": 500.0, "status": "Active" },
    "amount": 200.0
  },
  "state": {
    "Account": [
      { "id": "1", "balance": 1000.0, "status": "Active" },
      { "id": "2", "balance": 500.0, "status": "Active" }
    ]
  }
}

Success response (200 OK)

{
  "ok": true,
  "new_params": {
    "from": { "id": "1", "balance": 800.0, "status": "Active" },
    "to": { "id": "2", "balance": 700.0, "status": "Active" },
    "amount": 200.0
  },
  "violations": []
}

The new_params object reflects state after postconditions have been applied. Postconditions with the pattern param.field == old(param.field) +/- expr are extracted as state assignments.

Violation response (422 Unprocessable Entity)

When a contract is violated, the server returns 422 with details:

{
  "ok": false,
  "new_params": {
    "from": { "id": "1", "balance": 50.0, "status": "Active" },
    "to": { "id": "2", "balance": 500.0, "status": "Active" },
    "amount": 200.0
  },
  "violations": [
    {
      "kind": "precondition_failed",
      "message": "precondition failed: from.balance >= amount"
    }
  ]
}

Violation kinds:

Execution pipeline

Each request goes through four stages in order:

1. Preconditions — Evaluate requires expressions. If any fail, return violations immediately (no state change).
2. Edge guards — Evaluate edge_cases guards. If any match, return violations immediately.
3. State transformation — Extract assignments from ensures clauses (patterns like param.field == old(param.field) - amount) and apply them to produce new_params.
4. Postcondition + invariant validation — Evaluate all ensures and invariant expressions against the new state. Collect any violations.

How old() works at runtime

In postconditions, old(expr) evaluates expr against the pre-action parameter values. For example, given:

ensures {
  from.balance == old(from.balance) - amount
}

If from.balance was 1000.0 before the action and amount is 200.0, then old(from.balance) evaluates to 1000.0, and the runtime verifies that from.balance in the new state equals 800.0.

Status codes

cURL example

curl -X POST http://127.0.0.1:3000/actions/Transfer \
  -H "Content-Type: application/json" \
  -d '{
    "params": {
      "from": {"id": "1", "balance": 1000.0, "status": "Active"},
      "to": {"id": "2", "balance": 500.0, "status": "Active"},
      "amount": 200.0
    },
    "state": {
      "Account": [
        {"id": "1", "balance": 1000.0, "status": "Active"},
        {"id": "2", "balance": 500.0, "status": "Active"}
      ]
    }
  }'

Notes

• The server is single-threaded and blocking (via tiny_http). It's designed for development, testing, and demos — not production traffic.
• Stateless: the server stores nothing between requests. The caller owns all state.
• Union types are represented as strings (e.g., "Active", not {"variant": "Active"}).
• Multi-file specs with use imports are resolved at startup before serving.

Scaffolding a New Spec

intent init

Creates a new .intent file with a starter template including an example entity, action, and invariant.

Options

Examples

# Use directory name as module name
intent init

# Specify a module name
intent init --name Payments

# Specify both name and output path
intent init --name Payments -o specs/payments.intent

Generated template

Running intent init --name Payments creates payments.intent:

module Payments

--- TODO: Describe what this module specifies.

entity Example {
  id: UUID
  name: String
  status: Active | Inactive
}

action CreateExample {
  name: String

  requires {
    name != ""
  }

  ensures {
    exists e: Example => e.name == name
  }
}

invariant UniqueNames {
  forall a: Example => forall b: Example =>
    a.id != b.id => a.name != b.name
}

The template gives you working examples of each major construct. Replace them with your own entities, actions, and invariants.

Behavior

• The module name's first letter is automatically capitalized
• If the output file already exists, the command exits with an error (no overwriting)
• Without --name, the module name is derived from the current directory name

Shell Completions

intent completions <shell>

Generates tab-completion scripts for your shell. Completions cover all subcommands, flags, and options.

Supported shells

Setup

The command writes the completion script to stdout. Redirect it to the appropriate location for your shell.

Bash

intent completions bash | sudo tee /usr/share/bash-completion/completions/intent > /dev/null
source /usr/share/bash-completion/completions/intent

Or for the current user only:

mkdir -p ~/.local/share/bash-completion/completions
intent completions bash > ~/.local/share/bash-completion/completions/intent

Zsh

intent completions zsh > ~/.zfunc/_intent

Make sure ~/.zfunc is in your fpath (add fpath=(~/.zfunc $fpath) to ~/.zshrc before compinit).

Fish

intent completions fish > ~/.config/fish/completions/intent.fish

PowerShell

intent completions powershell >> $PROFILE

What's covered

Completions include:

• All subcommands (check, render, compile, verify, serve, etc.)
• Flags and options for each subcommand (--write, --check, --addr, etc.)
• Global options (--output, --help, --version)

Editor Integration

IntentLang ships with a VSCode extension and Language Server Protocol (LSP) server for a rich editing experience.

Features

Setup

1. Install the LSP server

# From source
cargo install --path crates/intent-lsp

# Or, if published to crates.io
cargo install intent-lsp

This installs the intent-lsp binary to your Cargo bin directory (typically ~/.cargo/bin/).

2. Install the VSCode extension

cd editors/vscode
npm install
npm run compile

Then in VSCode: Command Palette (Ctrl+Shift+P) > "Developer: Install Extension from Location..." > select the editors/vscode/ directory.

3. Open a .intent file

Open any .intent file and the extension activates automatically. If the intent-lsp binary is on your PATH, you'll get full LSP features.

Configuration

The extension provides two settings:

How It Works

The LSP server (intent-lsp) runs as a stdio process. When you open a .intent file:

1. The extension spawns the intent-lsp binary
2. On every file change, the server re-parses and re-checks the file
3. Parse errors and semantic diagnostics are pushed back as editor squiggles
4. Hover, completion, and go-to-definition requests are handled against the cached AST

For files with use imports, the server resolves imported modules from disk and runs cross-module type checking.

Cursor

Cursor is a VS Code fork with built-in AI features. The IntentLang extension works identically in Cursor since it is fully compatible with VS Code extensions.

Setup

The setup process is the same as VS Code:

1. Install the LSP server (see above)
2. Build the extension:

   cd editors/vscode
   npm install
   npm run compile
   

3. Install the extension: In Cursor, open the Command Palette (Ctrl+Shift+P / Cmd+Shift+P) > "Developer: Install Extension from Location..." > select the editors/vscode/ directory.
4. Open a .intent file and the extension activates automatically.

Configuration

All VS Code settings work the same in Cursor:

Cursor Rules for AI-Assisted Development

The IntentLang repo includes .cursor/rules/ files that teach Cursor's AI about the project:

• intentlang-syntax.mdc -- Activates for .intent files. Teaches Cursor's AI the IntentLang syntax, type system, expression grammar, and common mistakes to avoid. Enables AI-assisted writing and editing of .intent specs.
• project-conventions.mdc -- Activates for Rust source files and .pest grammar files. Teaches Cursor's AI the codebase structure, crate responsibilities, dependency graph, and development conventions.

These rules are checked into the repository so all contributors get them automatically.

Without the LSP

If the intent-lsp binary is not installed, you still get:

• Syntax highlighting (TextMate grammar)
• Code snippets
• Bracket matching, folding, and auto-indentation
• Comment toggling (Ctrl+/)

A warning message will suggest installing the LSP server for full functionality.

Four-Layer Design

IntentLang is built around four distinct layers. Layers 0 and 1 are both human-facing — the system meets users at their comfort level.

Layer 0: Natural Language (human-facing)

A natural language interface where humans describe what they want in plain English. An AI agent translates the description into a formal .intent spec.

Design goals:

• Lowest-barrier entry point — anyone can describe an idea
• Automated validation: generated specs are checked before output
• Confidence levels control how much the agent asks vs. assumes
• Edit mode for modifying existing specs from natural language
• Prompt preservation: original ask stored alongside the spec in version control

Layer 1: Intent Layer (human-facing)

A declarative specification language where humans express what they want and what constraints must hold, without prescribing implementation. Humans can author specs directly here, or refine specs generated from Layer 0.

Design goals:

• Readable by non-engineers (PMs, designers, stakeholders)
• Formally parseable and machine-interpretable
• Supports behavioral specs, not just type signatures
• Versioned and diffable

Layer 2: Agent IR (agent-facing)

A dense, formally verifiable intermediate representation that agents generate, optimize, and maintain.

Design goals:

• Machine-verifiable, compact, and unambiguous
• Not designed for human authoring — think typed AST with embedded proofs
• Every node carries source traces back to the spec layer
• Supports structural verification and coherence analysis

Layer 3: Audit Bridge

Tooling that maps between the two layers so humans can review, approve, and understand agent-produced code at the specification level.

Key properties:

• Every IR construct traces to a spec requirement
• Orphan code (implementation without spec justification) is a first-class error
• Coverage analysis shows which spec items have IR backing

The analogy

Humans describe the idea. The system formalizes it into a contract. Agents write the implementation. The toolchain proves the implementation satisfies the contract.

Why four layers?

Vibe coding collapses everything into a single step: prompt in, code out. That works for prototypes, but breaks down when correctness matters — there's nothing to verify against, no way to audit what the agent did, and no shared artifact for the team to review.

IntentLang separates concerns so that each participant works at the right level of abstraction. Humans own the spec (Layers 0–1). Agents own the implementation (Layer 2). The audit bridge (Layer 3) keeps both sides honest. The result is agentic engineering: AI-generated code with the same rigor you'd expect from a human-authored system.

Crate Structure

IntentLang is a Rust workspace with eight crates:

intent-cli ──→ intent-parser ←── intent.pest (PEG grammar)
    │              ↑
    ├──→ intent-check
    ├──→ intent-render
    ├──→ intent-ir (lowering, verification, audit, diff, incremental, lock)
    ├──→ intent-gen (NL → .intent, Layer 0)
    └──→ intent-runtime (stateless execution, HTTP server)

intent-lsp ──→ intent-parser, intent-check (LSP server)

intent-parser

PEG grammar (via pest) and AST definitions. Parses .intent files into a typed AST with source spans on every node. Includes a module resolver for use imports (DFS with cycle detection).

Key modules: ast.rs (AST node types), parser.rs (pest parser wrapper), resolve.rs (module resolver)

intent-check

Six-pass semantic analyzer. Validates type references, field access, quantifier bindings, old() placement, and more. Supports cross-module type checking via check_file_with_imports(). Produces diagnostic errors via miette.

Key modules: types.rs (type checking), constraints.rs (constraint validation)

intent-render

Renders parsed specs to Markdown, self-contained HTML, or canonical .intent source (formatter). Produces entity field tables, action signatures, and formatted invariants.

Key modules: markdown.rs, html.rs, format.rs

intent-ir

AST-to-IR lowering, structural verification, coherence analysis, audit bridge, spec diffing, incremental verification, and multi-agent locking. Every IR node carries a SourceTrace linking back to the original spec.

Key modules: lower.rs (AST → IR), verify.rs (verification), audit.rs (audit bridge), diff.rs (spec diffs), incremental.rs (cached verification), lock.rs (multi-agent claims)

intent-gen

Translates natural language descriptions into validated .intent specs via any OpenAI-compatible LLM API. Includes a generate-check-retry loop that feeds parse/check errors back to the LLM for correction.

Key modules: prompt.rs (system prompt), client.rs (LLM API client), validate.rs (generation loop)

intent-runtime

Stateless execution engine. Evaluates expressions against concrete JSON values, enforces pre/postconditions and invariants, and auto-generates REST endpoints from actions via HTTP server.

Key modules: eval.rs (expression evaluator), contract.rs (contract evaluation), serve.rs (HTTP server)

intent-lsp

Language Server Protocol server using tower-lsp and tokio. Provides real-time diagnostics, go-to-definition, hover, and context-aware completion for .intent files. Used by the VSCode extension.

Key modules: server.rs (LSP backend), document.rs (per-file state + line index), diagnostics.rs, hover.rs, navigation.rs, completion.rs

intent-cli

CLI entry point using clap (derive). Wires together all other crates and exposes subcommands: check, render, render-html, compile, verify (--incremental), audit, coverage, diff, query, lock, unlock, status, fmt, init, completions, generate, serve. Supports --output json for agent consumption.

Published crates

Seven crates are published to crates.io:

• intent-parser
• intent-check
• intent-render
• intent-ir
• intent-gen
• intent-runtime
• intent-cli

Fund Transfer

A fund transfer system between accounts within the same currency. Demonstrates entities with union-typed status fields, actions with pre/postconditions, conservation invariants, and edge cases.

File: examples/transfer.intent

module TransferFunds

--- A fund transfer system between accounts within the same currency.
--- Supports basic account-to-account transfers with balance validation,
--- idempotency guarantees, and manager approval for large amounts.

entity Account {
  id: UUID
  owner: String
  balance: Decimal(precision: 2)
  currency: CurrencyCode
  status: Active | Frozen | Closed
  created_at: DateTime
}

entity TransferRecord {
  id: UUID
  request_id: UUID
  from_account: Account
  to_account: Account
  amount: Decimal(precision: 2)
  status: Pending | Completed | Failed | Reversed
  created_at: DateTime
  completed_at: DateTime?
}

action Transfer {
  --- Move funds from one account to another.
  from: Account
  to: Account
  amount: Decimal(precision: 2)
  request_id: UUID

  requires {
    from.status == Active
    to.status == Active
    from.currency == to.currency
    amount > 0
    from.balance >= amount
    from.id != to.id
  }

  ensures {
    from.balance == old(from.balance) - amount
    to.balance == old(to.balance) + amount
    exists r: TransferRecord =>
      r.request_id == request_id &&
      r.status == Completed
  }

  properties {
    idempotent: true
    idempotency_key: request_id
    atomic: true
    audit_logged: true
    max_latency_ms: 500
  }
}

action FreezeAccount {
  --- Freeze an account, preventing all transfers.
  account: Account
  reason: String

  requires {
    account.status == Active
  }

  ensures {
    account.status == Frozen
  }

  properties {
    audit_logged: true
    requires_role: "compliance_officer"
  }
}

invariant NoNegativeBalances {
  --- No account may ever have a negative balance.
  forall a: Account => a.balance >= 0
}

invariant TransferConservation {
  --- Transfers must not create or destroy money.
  forall t: Transfer =>
    old(t.from.balance) + old(t.to.balance) ==
    t.from.balance + t.to.balance
}

edge_cases {
  when amount > 10000.00 => require_approval(level: "manager")
  when from.owner == to.owner => allow(note: "Self-transfer between own accounts")
  when from.currency != to.currency => reject("Cross-currency transfers not supported.")
}

Key concepts demonstrated

• Union types for entity status: Active | Frozen | Closed
• old() in ensures for state transition assertions
• Conservation invariant ensuring transfers don't create or destroy money
• Properties for runtime metadata (idempotency, atomicity, latency SLAs)
• Edge cases for approval workflows and error conditions

Authentication

A user authentication system with password-based login, session management, and brute-force protection. Demonstrates existential quantifiers, domain functions, and rate limiting.

File: examples/auth.intent

module Authentication

--- User authentication system with password-based login,
--- session management, and brute-force protection.

entity User {
  id: UUID
  email: Email
  password_hash: String
  status: Active | Suspended | Deactivated
  failed_attempts: Int
  locked_until: DateTime?
  last_login: DateTime?
  created_at: DateTime
}

entity Session {
  id: UUID
  user: User
  token: String
  expires_at: DateTime
  created_at: DateTime
  revoked: Bool
}

action Login {
  --- Authenticate a user with email and password.
  email: Email
  password: String

  requires {
    exists u: User => u.email == email
    lookup(User, email).status == Active
    lookup(User, email).locked_until == null ||
      lookup(User, email).locked_until < now()
  }

  ensures {
    when password_verified(password, lookup(User, email).password_hash) =>
      exists s: Session =>
        s.user.email == email &&
        s.revoked == false &&
        s.expires_at > now()
      &&
      lookup(User, email).failed_attempts == 0
      &&
      lookup(User, email).last_login == now()

    when !password_verified(password, lookup(User, email).password_hash) =>
      lookup(User, email).failed_attempts ==
        old(lookup(User, email).failed_attempts) + 1
  }

  properties {
    audit_logged: true
    rate_limited: { max: 10, window_seconds: 60, key: email }
    sensitive_fields: [password]
  }
}

action Logout {
  --- End a user session.
  session: Session

  requires {
    session.revoked == false
    session.expires_at > now()
  }

  ensures {
    session.revoked == true
  }

  properties {
    idempotent: true
    audit_logged: true
  }
}

invariant MaxFailedAttempts {
  --- Lock accounts after 5 consecutive failed login attempts.
  forall u: User =>
    u.failed_attempts >= 5 => u.locked_until != null
}

invariant SessionExpiry {
  --- All active sessions must have a future expiration.
  forall s: Session =>
    s.revoked == false => s.expires_at > now()
}

edge_cases {
  when lookup(User, email).status == Suspended =>
    reject("Account suspended. Contact support.")
  when lookup(User, email).status == Deactivated =>
    reject("Account deactivated.")
  when lookup(User, email).failed_attempts >= 5 =>
    reject("Account locked due to too many failed attempts.")
}

Key concepts demonstrated

• Domain functions like lookup(), now(), password_verified()
• Conditional postconditions using when ... => in ensures blocks
• Existential quantifiers in both requires and ensures
• Implication in invariants (failed_attempts >= 5 => locked_until != null)
• Rate limiting and sensitive fields as action properties

Shopping Cart

A shopping cart system with item management, quantity updates, and checkout with inventory validation. Demonstrates collection types, nested entity references, and multiple related actions.

File: examples/shopping_cart.intent

module ShoppingCart

--- A shopping cart system supporting item management,
--- quantity updates, and checkout with inventory validation.

entity Product {
  id: UUID
  name: String
  price: Decimal(precision: 2)
  stock: Int
  status: Available | Discontinued
}

entity CartItem {
  product: Product
  quantity: Int
}

entity Cart {
  id: UUID
  owner: UUID
  items: List<CartItem>
  created_at: DateTime
  checked_out: Bool
}

entity Order {
  id: UUID
  cart: Cart
  total: Decimal(precision: 2)
  status: Pending | Confirmed | Shipped | Delivered | Cancelled
  created_at: DateTime
}

action AddItem {
  --- Add a product to the cart, or increase quantity if already present.
  cart: Cart
  product: Product
  quantity: Int

  requires {
    cart.checked_out == false
    product.status == Available
    quantity > 0
    product.stock >= quantity
  }

  ensures {
    exists item: CartItem =>
      item.product == product &&
      item.quantity == quantity
  }

  properties {
    idempotent: false
  }
}

action RemoveItem {
  --- Remove a product from the cart entirely.
  cart: Cart
  product: Product

  requires {
    cart.checked_out == false
    exists item: CartItem =>
      item.product == product
  }

  ensures {
    !(exists item: CartItem =>
      item.product == product)
  }
}

action UpdateQuantity {
  --- Change the quantity of an item already in the cart.
  cart: Cart
  product: Product
  new_quantity: Int

  requires {
    cart.checked_out == false
    new_quantity > 0
    product.stock >= new_quantity
    exists item: CartItem =>
      item.product == product
  }

  ensures {
    exists item: CartItem =>
      item.product == product &&
      item.quantity == new_quantity
  }
}

action Checkout {
  --- Convert the cart into a confirmed order.
  cart: Cart

  requires {
    cart.checked_out == false
    forall item: CartItem =>
      item.product.stock >= item.quantity
  }

  ensures {
    cart.checked_out == true
    exists o: Order =>
      o.cart == cart &&
      o.status == Confirmed
  }

  properties {
    atomic: true
    audit_logged: true
  }
}

invariant StockNonNegative {
  --- Product stock can never go below zero.
  forall p: Product => p.stock >= 0
}

invariant CartItemsPositive {
  --- Every item in a cart must have a positive quantity.
  forall item: CartItem => item.quantity > 0
}

edge_cases {
  when product.status == Discontinued => reject("Product is no longer available")
  when product.stock < quantity => reject("Insufficient stock")
  when cart.checked_out == true => reject("Cart has already been checked out")
}

Key concepts demonstrated

• Collection types (List<CartItem>)
• Nested entity references (item.product.stock)
• Negated existentials in postconditions (!(exists ...))
• Quantifiers in preconditions (forall item: CartItem => ... in Checkout)
• Multiple related actions forming a complete workflow (add, remove, update, checkout)