Crate elicitation

Expand description

Conversational elicitation of strongly-typed Rust values via MCP.

The elicitation library provides a trait-based system for eliciting strongly-typed values from users through conversational interaction via the Model Context Protocol (MCP). It transforms LLM conversations into type-safe Rust values with compile-time guarantees.

§MCP Setup Required

This library runs as an MCP server and requires an MCP client (like Claude Desktop or Claude CLI) to provide the elicitation tools. Your application won’t work standalone - it must be invoked by an MCP client.

See the README for setup instructions.

§Core Concepts

§Traits

Prompt - Provides prompt metadata for a type
Elicit - Main trait for eliciting values

§Interaction Paradigms

Select - Choose from finite options (enum pattern)
Affirm - Yes/no confirmation (bool pattern)
Survey - Multi-field elicitation (struct pattern)
Authorize - Permission policies (planned for v0.2.0)

§Example

use elicitation::{Elicitation, ElicitResult};
use rmcp::service::{Peer, RoleClient};

async fn example(client: &Peer<RoleClient>) -> ElicitResult<()> {
    // Elicit a simple integer
    let age: i32 = i32::elicit(communicator).await?;

    // Elicit an optional value
    let nickname: Option<String> = Option::<String>::elicit(communicator).await?;

    // Elicit a collection
    let scores: Vec<i32> = Vec::<i32>::elicit(communicator).await?;
    Ok(())
}

§Derive Macros

The library provides derive macros for automatic implementation:

use elicitation::Elicit;

// Enums automatically use the Select paradigm
#[derive(Elicit)]
enum Color {
    Red,
    Green,
    Blue,
}

// Structs automatically use the Survey paradigm
#[derive(Elicit)]
struct Person {
    #[prompt("What is your name?")]
    name: String,
    #[prompt("What is your age?")]
    age: u8,
}

§MCP Integration

The library uses the rmcp crate - the official Rust MCP SDK - for MCP client integration. All elicitation happens through asynchronous MCP tool calls.

Re-exports§

pub use prompt_tree::AssembledPrompt;
pub use prompt_tree::ElicitPromptTree;
pub use prompt_tree::PromptKind;
pub use prompt_tree::PromptTree;
pub use prompt_tree::collect_assembled_prompts;
pub use plugin::DescriptorPlugin;
pub use plugin::ElicitPlugin;
pub use plugin::NoContext;
pub use plugin::PluginContext;
pub use plugin::PluginToolRegistration;
pub use plugin::StatefulPlugin;
pub use plugin::ToolDescriptor;
pub use plugin::make_descriptor;
pub use plugin::make_descriptor_ctx;
pub use dynamic::AnyToolFactory;
pub use dynamic::AnyToolSlot;
pub use dynamic::ContextualFactory;
pub use dynamic::DynamicToolDescriptor;
pub use dynamic::DynamicToolRegistry;
pub use dynamic::ToolFactoryRegistration;
pub use dynamic::TypedSlot;
pub use verification::types::ValidationError;
pub use type_graph::TypeGraphKey;
pub use type_graph::all_graphable_types;
pub use type_graph::lookup_type_graph;
pub use type_spec::ElicitSpec;
pub use type_spec::SpecCategory;
pub use type_spec::SpecCategoryBuilder;
pub use type_spec::SpecEntry;
pub use type_spec::SpecEntryBuilder;
pub use type_spec::TypeSpec;
pub use type_spec::TypeSpecBuilder;
pub use type_spec::TypeSpecInventoryKey;
pub use type_spec::i32_as_i8_checked;
pub use type_spec::lookup_type_spec;
pub use type_spec::lookup_type_spec_by_id;
pub use type_spec::type_spec_plugin::TypeSpecPlugin;
pub use contracts::And;
pub use contracts::Established;
pub use contracts::FormalMethod;
pub use contracts::Implies;
pub use contracts::InVariant;
pub use contracts::Is;
pub use contracts::KaniVariantConstruction;
pub use contracts::KaniVariantState;
pub use contracts::Prop;
pub use contracts::ProvableFrom;
pub use contracts::Refines;
pub use contracts::VerifiedStateMachine;
pub use contracts::VerifiedTransition;
pub use contracts::both;
pub use contracts::downcast;
pub use contracts::fst;
pub use contracts::snd;
pub use tool::Tool;
pub use tool::True;
pub use tool::both_tools;
pub use tool::then;
pub use verification::Contract;
pub use verification::types::ArcNonNull;
pub use verification::types::ArcSatisfies;
pub use verification::types::ArrayAllSatisfy;
pub use verification::types::BTreeMapNonEmpty;
pub use verification::types::BTreeSetNonEmpty;
pub use verification::types::BoolFalse;
pub use verification::types::BoolTrue;
pub use verification::types::BoxNonNull;
pub use verification::types::BoxSatisfies;
pub use verification::types::CharAlphabetic;
pub use verification::types::CharAlphanumeric;
pub use verification::types::CharNumeric;
pub use verification::types::DurationNonZero;
pub use verification::types::DurationPositive;
pub use verification::types::F32Finite;
pub use verification::types::F32NonNegative;
pub use verification::types::F32Positive;
pub use verification::types::F64Finite;
pub use verification::types::F64NonNegative;
pub use verification::types::F64Positive;
pub use verification::types::HashMapNonEmpty;
pub use verification::types::HashSetNonEmpty;
pub use verification::types::I8NonNegative;
pub use verification::types::I8NonZero;
pub use verification::types::I8NonZeroStyle;
pub use verification::types::I8Positive;
pub use verification::types::I8Range;
pub use verification::types::I8RangeStyle;
pub use verification::types::I16NonNegative;
pub use verification::types::I16NonZero;
pub use verification::types::I16NonZeroStyle;
pub use verification::types::I16Positive;
pub use verification::types::I16Range;
pub use verification::types::I16RangeStyle;
pub use verification::types::I32NonNegative;
pub use verification::types::I32NonZero;
pub use verification::types::I32Positive;
pub use verification::types::I32Range;
pub use verification::types::I32RangeStyle;
pub use verification::types::I64NonNegative;
pub use verification::types::I64NonZero;
pub use verification::types::I64Positive;
pub use verification::types::I64Range;
pub use verification::types::I64RangeStyle;
pub use verification::types::I128NonNegative;
pub use verification::types::I128NonZero;
pub use verification::types::I128Positive;
pub use verification::types::I128Range;
pub use verification::types::I128RangeStyle;
pub use verification::types::IpPrivate;
pub use verification::types::IpPublic;
pub use verification::types::IpV4;
pub use verification::types::IpV6;
pub use verification::types::Ipv4Loopback;
pub use verification::types::Ipv6Loopback;
pub use verification::types::IsizeNonNegative;
pub use verification::types::IsizeNonZero;
pub use verification::types::IsizePositive;
pub use verification::types::IsizeRange;
pub use verification::types::IsizeRangeStyle;
pub use verification::types::LinkedListNonEmpty;
pub use verification::types::OptionSome;
pub use verification::types::PathBufExists;
pub use verification::types::PathBufIsDir;
pub use verification::types::PathBufIsFile;
pub use verification::types::PathBufReadable;
pub use verification::types::RcNonNull;
pub use verification::types::RcSatisfies;
pub use verification::types::ResultOk;
pub use verification::types::StringNonEmpty;
pub use verification::types::Tuple2;
pub use verification::types::Tuple3;
pub use verification::types::Tuple4;
pub use verification::types::U8NonZero;
pub use verification::types::U8Positive;
pub use verification::types::U8Range;
pub use verification::types::U8RangeStyle;
pub use verification::types::U16NonZero;
pub use verification::types::U16Positive;
pub use verification::types::U16Range;
pub use verification::types::U16RangeStyle;
pub use verification::types::U32NonZero;
pub use verification::types::U32Positive;
pub use verification::types::U32Range;
pub use verification::types::U32RangeStyle;
pub use verification::types::U64NonZero;
pub use verification::types::U64Positive;
pub use verification::types::U64Range;
pub use verification::types::U64RangeStyle;
pub use verification::types::U128NonZero;
pub use verification::types::U128Positive;
pub use verification::types::U128Range;
pub use verification::types::U128RangeStyle;
pub use verification::types::UsizeNonZero;
pub use verification::types::UsizePositive;
pub use verification::types::UsizeRange;
pub use verification::types::UsizeRangeStyle;
pub use verification::types::VecAllSatisfy;
pub use verification::types::VecDequeNonEmpty;
pub use verification::types::VecNonEmpty;
pub use verification::mechanisms::AffirmReturnsBoolean;
pub use verification::mechanisms::InputNonEmpty;
pub use verification::mechanisms::MechanismWithType;
pub use verification::mechanisms::NumericReturnsValid;
pub use verification::mechanisms::SurveyReturnsValidVariant;
pub use verification::mechanisms::TextReturnsNonEmpty;
pub use verification::mechanisms::TextReturnsString;
pub use rmcp;

Modules§

contracts: Proof-carrying composition primitives.
dynamic: DynamicToolRegistry — runtime middleware between inventory and the MCP server.
emit_code: Code recovery — emit verified workflows as Rust source.
kani_compose: Compositional depth-bounded construction for Kani proofs.
mcp: MCP (Model Context Protocol) integration.
middleware: Communicator middleware — transparent wrappers that enhance any ElicitCommunicator with context accumulation, observability, etc.
plugin: Type-erased plugin interface for the elicitation tool registry.
prompt_tree: Static prompt tree for Elicitation types.
style: Elicitation style system - separates UX from behavior.
tool: Contract-based tool system for MCP.
type_graph: Type graph visualization for elicitation workflows.
type_spec: Type specification layer for agent-accessible type exploration.
verification: Formal verification framework for tool chains.

Macros§

default_style: Generate a default-only style enum for a type.
elicit_newtype: Generates a transparent newtype wrapper around a third-party type.
elicit_newtype_methods: Generates both newtype and method wrappers with MCP tools.
elicit_newtype_traits: Forwards standard library traits from the inner type to an elicit_newtype! wrapper.
elicit_newtypes: Generates multiple newtype wrappers in bulk.
elicit_router: Creates an aggregator struct that registers elicit_checked tools from multiple types.
elicit_tools: Generates elicitation tool methods inside an existing #[tool_router] impl block.
kani_label: Produce a label string for display / diagnostics in formal-method transitions.
proof_credential: Declare one or more proof-credential ZST types and wire each to its proposition.
register_emit: Register a params type with the global emit registry under a tool name.
select_trenchcoat: Generates a Select-aware newtype wrapper for a foreign enum.
select_trenchcoat_traits: Forwards standard library traits from the inner type to a select_trenchcoat! wrapper.

Structs§

ChoiceSet: A set of choices for elicitation.
DurationGenerator: Generator for creating Duration values with a specified strategy.
ElicitBuilder: Builder for one-off style overrides.
ElicitClient: Client wrapper that carries style context.
ElicitError: Elicitation error with location tracking.
ElicitServer: Server wrapper that carries style context.
ElicitToolDescriptor: Describes an elicit tool that can be registered with MCP.
ElicitToolOutput: Wrapper that ensures MCP-compliant object schemas for any type.
ElicitationContext: Storage for current elicitation context (for observability).
FieldInfo: Metadata for a single survey field.
Formatter: Formatting helper - unit struct with formatting methods.
IoErrorGenerator: Generator for creating std::io::Error instances for testing.
JsonError: JSON parsing error wrapper.
Parser: Parser helper - unit struct with parsing methods.
PluginRegistry: Aggregates multiple ElicitPlugin instances into one MCP server.
RmcpError: RMCP error wrapper.
ServiceError: RMCP ServiceError wrapper for error conversion.
StyleContext: Storage for type-specific styles.
SystemTimeGenerator: Generator for creating SystemTime values with a specified strategy.
Toolchain: A curated subset of a PluginRegistry, visible to agents.
TypeMetadata: Complete metadata describing a type’s elicitation structure.
Validator: Validation helper - unit struct with validation methods.
VariantMetadata: Metadata for one variant of a Select-pattern enum.

Enums§

DurationGenerationMode: Generation mode for Duration.
ElicitErrorKind: Specific error conditions during elicitation.
ElicitationPattern: The elicitation pattern used by a type.
IoErrorGenerationMode: Generation mode for std::io::Error.
PatternDetails: Pattern-specific structural details.
StringStyle: Elicitation style variants for String.
SystemTimeGenerationMode: Generation mode for SystemTime.

Traits§

Affirm: Binary confirmation (yes/no, true/false pattern).
Authorize: Permission-granting interaction with policy choices.
ElicitCommunicator: Abstraction for elicitation communication.
ElicitComplete: Compiler-enforced supertrait for fully-implemented elicitation support.
ElicitIntrospect: Static introspection into a type’s elicitation structure.
ElicitJson: Single-shot JSON elicitation for types with a known schema.
ElicitProxy: Bridge a type to its serializable elicit proxy.
Elicitation: Main elicitation trait - entry point for value elicitation.
Filter: Collection-level filtering for selection options.
Generator: Trait for generating values of a type.
Prompt: Shared metadata for prompts across all elicitation patterns.
Select: Select one value from a finite set (dropdown/radio button pattern).
StyleMarker: Marker trait for elicitation style types.
Survey: Multi-field structured elicitation (form/wizard pattern).
VerifiedWorkflow: Compiler-enforced supertrait for fully-proven workflow propositions.

Functions§

collect_all_elicit_tools: Collect all elicit tools registered via #[derive(Elicit)].

Type Aliases§

ElicitResult: Convenience alias for elicitation results.

Attribute Macros§

elicit_tool
formal_method: Mark a function as a contract-honoring formal method and generate backend verification harnesses.
formal_method_test_v1: V1: pass the function through completely unchanged — baseline, no warnings expected.
formal_method_test_v2: V2: wrap in mod + pub use (the mod wrapper alone) — no cfg tokens emitted.
formal_method_test_v3: V3: mod wrapper + transform #[instrument] into cfg_attr(not(any(kani,creusot)), instrument).
formal_method_test_v4: V4: V3 + also emit an empty #[allow] const _: () = {} (like gated_kani_harness empty case).
formal_method_test_v5: V5: V4 + emit a real kani harness const (cfg(kani) inside allow const).
formal_method_test_v6: V6: put #[allow(unexpected_cfgs)] directly on the function (no mod wrapper). Tests whether allow on the item itself suppresses proc-macro-origin warnings.
formal_method_test_v7: V7: #[allow(unexpected_cfgs)] on both the outer mod AND directly on the function inside.
formal_method_test_v8: V8: mod wrapper, but pass #[instrument] through UNCHANGED (no cfg_attr transform). Tests whether the cfg_attr transform itself is the warning source.
formal_method_test_v9: V9: strip #[instrument] entirely, manually inject tracing::info_span! into body. No cfg_attr emitted → zero unexpected_cfgs warnings. Kani/Creusot run on the plain function body without tracing attribute overhead.

Derive Macros§

Elicit: Derive the Elicit trait for enums (→ Select) or structs (→ Survey).
ElicitPlugin: Generate a ToolDescriptor companion function from an async tool handler.
ElicitTestE1
ElicitTestE2
ElicitTestE3
ElicitTestE4
ElicitTestE5
ElicitTestE6
ElicitTestE7
ElicitTestE8
ElicitTestE9
ElicitTestE10
ElicitTestE11
ElicitTestE12
ElicitTestE13
KaniCompose: Derive the Prop trait for a zero-cost typestate marker.
KaniVariantState: Derive KaniVariantState for a VSM state enum.
Prop
ToCodeLiteral: Derive ToCodeLiteral for structs and enums.
VerifiedStateMachine: Derive VerifiedStateMachine for a unit struct, inferring State and Invariant from naming conventions and wiring transition_harnesses() from a #[vsm(transitions = [...])] attribute.