Skip to content
Lexicon

Creating Your First Contract

This tutorial walks through creating a contract for a simple key-value store component.

Prerequisites

Section titled “Prerequisites”
  • Lexicon installed (cargo install --path crates/cli)
  • A Rust project initialized with lexicon init
  • Authenticated with an AI provider (lexicon auth login)

Step 1: Start a Chat Session

Section titled “Step 1: Start a Chat Session”
Terminal window
lexicon

This starts an interactive design session. Describe what you want to build:

you> I need a contract for a basic key-value store with get, set, and delete operations

The AI will create a contract with the appropriate invariants, required semantics, forbidden behaviors, and edge cases.

Step 2: Review the Generated Contract

Section titled “Step 2: Review the Generated Contract”

The AI creates a contract and explains what it contains:

  • Invariants — conditions that must always hold (e.g., “a key set with a value must return that value on get”)
  • Required semantics — behaviors the implementation must provide (e.g., “get(key) returns None for missing keys”)
  • Forbidden semantics — behaviors that must never occur (e.g., “must not panic on missing key lookup”)
  • Edge cases — specific scenarios with expected behavior (e.g., “setting the same key twice overwrites the first value”)

The contract is saved to specs/contracts/key-value-store.toml.

Step 3: Refine the Contract

Section titled “Step 3: Refine the Contract”

The AI will proactively suggest gaps in your specification. You can also ask for changes:

you> Add a forbidden behavior: must not leak memory on repeated set/delete cycles
you> Change inv-001 severity to required

The AI updates the contract file using the UPDATE_CONTRACT directive.

Step 4: Generate Conformance Tests

Section titled “Step 4: Generate Conformance Tests”

Ask the AI to generate conformance tests:

you> Generate conformance tests for key-value-store

This generates a test harness at tests/conformance/key_value_store.rs with stub test functions for each invariant, required semantic, and forbidden semantic.

Step 5: Sync to CLAUDE.md

Section titled “Step 5: Sync to CLAUDE.md”
you> Sync CLAUDE.md

Your contract’s invariants, required semantics, and forbidden semantics are now included in the AI context via the SYNC_CLAUDE directive.

Step 6: Verify

Section titled “Step 6: Verify”

Exit the chat session and run verification:

Terminal window
lexicon verify

Next Steps

Section titled “Next Steps”
  • Fill in the generated conformance test stubs with real assertions
  • Run lexicon verify to check your implementation against the contract
  • Set up CI integration to verify on every push
  • Promote the contract from draft to active when ready