Elicitation

Structured agent interaction backed by formal verification.

What is Elicitation?

An MCP agent calling your tools can pass anything, in any order. Elicitation inverts that: instead of the agent pushing arbitrary values into your functions, your types pull values from the agent through a verified round-trip. The agent sees a prompt; you get a validated, type-safe result. That is what elicit() does.

The rest of the framework builds on that foundation:

• Shadow crates give agents a verified vocabulary for third-party libraries
• Contracts make invalid workflow sequences fail at compile time, not runtime
• Verified State Machines combine all three into formally proven programs

Every participating type carries proofs for three independent verifiers (Kani, Verus, Creusot), composed automatically from its fields by #[derive(Elicit)].

Deriving Agent-Native Types

#[derive(Elicit)] generates elicit(), the MCP JSON schema, and proof methods by composing the impls of its fields. Add a field, get its proof for free:

#[derive(Debug, Clone, Serialize, Deserialize, JsonSchema, Elicit)]
pub enum Environment { Production, Staging, Development }

#[derive(Debug, Clone, Serialize, Deserialize, JsonSchema, Elicit)]
pub struct DeployConfig {
    #[prompt("Which environment?")]
    pub environment: Environment,

    #[prompt("Number of replicas (1–16):")]
    #[spec_requires("replicas >= 1 && replicas <= 16")]
    pub replicas: u8,

    #[skip]
    pub internal_id: u64,    // excluded from elicitation
}

DeployConfig::elicit(&server).await? drives a back-and-forth with the agent, prompting each field in turn and validating responses. The agent cannot skip fields or bypass constraints.

Interaction paradigms

The derive picks the right paradigm from the shape of the type:

Style System

A terse machine prompt is noise to a human; a friendly wizard prompt wastes an agent's context. Name your audience on the field — the derive generates the style enum; swap it at the call site:

#[prompt("environment")]
#[prompt("Which environment should we deploy to?",      style = "human")]
#[prompt("environment: production|staging|development", style = "agent")]
pub environment: Environment,

let config = DeployConfig::elicit(&client.with_style(DeployConfigElicitStyle::Human)).await?;

Generators

Generator<Target> produces values of a target type from any source — sensor fusion, lookup tables, physics steps. elicitation_rand adds #[rand(...)] field attributes (bounded(L, H), positive, nonzero, even, odd) and derives a seeded random_generator(seed: u64) for deterministic property testing, with its own Kani suite.

Shadow Crates — Familiar APIs Over MCP

A shadow crate (elicit_*) mirrors the API of its source library with MCP-compatible types and tools that use the same names and types developers already know. The goal is that an agent working with elicit_reqwest feels like it is working with reqwest — the vocabulary is familiar, the types correspond, but everything crosses the MCP boundary safely.

Each shadow crate exposes three layers:

#[reflect_methods]
pub struct ElicitArg(pub clap::Arg);
// Generates: arg__get_long, arg__get_short, arg__get_help, ... as MCP tools

For compile-time macros (e.g. sqlx::query!), fragment tools emit verified Rust source via EmitCode; the macro expands in the consumer binary where a live connection is available.

Contracts — Invariants as Types

Programs have invariants that hold regardless of execution path. Most frameworks leave them as comments or runtime checks — things developers know but the compiler doesn't. Elicitation makes them explicit in the type system.

A Prop is a marker type: a name for an invariant. Established<P> is a zero-sized proof token that P holds — it exists only because something produced it, and the only way to produce it is through a ProvableFrom exchange:

#[derive(Prop)] pub struct ConnectionReady;
#[derive(Prop)] pub struct QueryValidated;

// ProvableFrom is a sealed exchange: present ConnectionReady, receive QueryValidated
impl ProvableFrom<ConnectionReady> for QueryValidated { ... }

The exchange lives in a trait method — and that trait method is the only door to the token:

fn validate_query(
    &self,
    query: &str,
    _pre: Established<ConnectionReady>,   // credential required
) -> Result<(ValidatedQuery, Established<QueryValidated>), DbError> {
    // business logic that maintains the invariant — no other path exists
}

Because the trait method is the only constructor for Established<QueryValidated>, the business logic must run. The compiler enforces it. Proofs can then verify that this chain is sound.

And<P,Q> composes proofs; both(p, q) constructs conjunctions. Shadow crates ship their own Prop types: elicit_sqlx has DbConnected, QueryExecuted, TransactionOpen; elicit_reqwest has UrlValid, RequestCompleted, FetchSucceeded.

Verified State Machines

A Verified State Machine is a state machine where every state implements Elicitation and every transition is a #[formal_method]. That dual constraint is exactly what the derive needs to auto-generate proofs: all inputs and outputs are within the verified type system, and all transitions follow the ProvableFrom contract — so there is no path through the machine that the framework cannot inspect and verify.

// All states implement Elicitation
#[derive(Debug, Clone, VerifiedStateMachine)]
pub enum PanelState { Idle, Loading, Ready, Error }

// Consistency predicate — the invariant every transition must preserve
pub fn panel_consistent(state: &PanelState, data: &Option<Data>) -> bool {
    match state {
        PanelState::Ready => data.is_some(),
        PanelState::Idle  => data.is_none(),
        _                 => true,
    }
}

// All transitions are #[formal_method] — the only doors between states
impl PanelMachine {
    #[formal_method]
    pub fn begin_load(&mut self) -> Established<Loading> { ... }

    #[formal_method]
    pub fn finish_load(&mut self, data: Data, _pre: Established<Loading>)
        -> Established<Ready> { ... }
}

#[formal_method] gates #[instrument] so proof toolchains don't chase tracing internals, and registers the transition for harness generation. The generated proofs verify that every reachable transition preserves the consistency predicate — correctness by construction.

elicitation generate kani --crate-path crates/my_vsm/src --out crates/proofs/src/kani/generated
just prove   # runs all three backends

Formal Verification

The proof infrastructure is bottom-up. The core elicitation crate ships verified proofs for stdlib and third-party types behind feature gates — capturing meaningful bounds: a PortNumber is always in [1024, 65535]; a NonEmptyString always has length > 0; an Established<FetchSucceeded> is always produced from a 2xx response. When you derive Elicit on your own types, your proofs compose from those canonical proofs. A struct's proof is the union of its fields' proofs — add a field, get its verification bounds for free.

At the VSM level, proofs verify the richer claim: that every transition preserves the consistency predicate. Three verifiers approach this from independent directions:

just verify-kani-tracked
just verify-creusot <file.rs>
just verify-verus-tracked

Visibility

An agent working with an unfamiliar codebase can't read source. Three features expose the vocabulary at runtime without flooding the context window:

TypeSpec surfaces ElicitSpec annotations as MCP tools. describe_type returns a summary and list of available categories; explore_type returns one category — requires, ensures, bounds, fields — on demand. Agents pull only what they need.

TypeGraph renders structural hierarchies of registered types as Mermaid or DOT graphs. list_types() → graph_type("ApplicationConfig") shows how NetworkConfig, Role, and DeploymentMode compose into it, in one tool call.

ElicitIntrospect exposes zero-allocation pattern() and metadata() for labelling tracing spans and Prometheus metrics — no source parsing, no allocation:

ELICITATION_COUNTER
    .with_label_values(&[T::metadata().type_name, T::pattern().as_str()])
    .inc();

#[derive(Elicit)] registers types for all three via inventory::submit! automatically.

Getting Started

[dependencies]
elicitation = "0.11"
rmcp        = "1"
schemars    = "0.8"
serde       = { version = "1", features = ["derive"] }
tokio       = { version = "1", features = ["full"] }

Derive Elicit on your domain types, call elicit() inside a tool handler, and expose via elicit_tools!:

#[tool_router]
impl GameServer {
    #[tool(description = "Play a move")]
    pub async fn play(&self, peer: Peer<RoleServer>) -> Result<CallToolResult, ErrorData> {
        let server = ElicitServer::new(peer);

        // Elicit a validated struct — the agent cannot produce an invalid PlayerProfile
        let profile = PlayerProfile::elicit(&server).await?;

        // ChoiceSet: constrain to a runtime-computed set — agent cannot pick outside it
        let bet = ChoiceSet::new(vec![1u32, 5, 10, 25])
            .with_prompt("Choose your bet:")
            .elicit(&server).await?;

        Ok(CallToolResult::success(vec![Content::text(
            format!("{} bets {} on {:?}", profile.name, bet, profile.difficulty),
        )]))
    }

    // Auto-generate elicit_difficulty and elicit_player_profile tools
    elicitation::elicit_tools! { Difficulty, PlayerProfile }
}

Add shadow crate plugins alongside your own server via PluginRegistry:

PluginRegistry::new()
    .register_flat(GameServer::new())
    .register("http", elicit_reqwest::WorkflowPlugin::default_client())
    .register("db",   elicit_sqlx::SqlxWorkflowPlugin::default())
    .serve(rmcp::transport::stdio())
    .await?;

One registry, one transport, zero glue code.

Workspace Crate Map

Further Reading