elicitation (Crumplecup)

引出

经过形式验证的类型安全状态机。你可以证明的程序不变量。

   

______________________________________________________________________

故事

第一步：验证类型（枯燥但基础）

形式验证研究几乎完全集中在方法上——而且是永远的 原因。方法很有趣；类型不是。谁在乎呢 i8 是一个 i8?

然而：验证类型是可处理的。一种受约束的类型，如 PortNumber 或 StringNonEmpty 具有清晰的、机器可检查的不变量。当类型实现时 Elicitation，作为trait的一部分，它获得了三种证明方法——每种方法返回一个 TokenStream 相应的工具链可以验证：

#[cfg(feature = "proofs")]
fn kani_proof()    -> proc_macro2::TokenStream { /* symbolic execution proof */ }
fn verus_proof()   -> proc_macro2::TokenStream { /* SMT specification proof  */ }
fn creusot_proof() -> proc_macro2::TokenStream { /* deductive contract proof  */ }

这些不是单独证明文件上的注释。类型 *携带* 它的证据。 对于用户定义的类型， #[derive(Elicit)] 自动组成证明 组成字段类型的证明——添加一个字段，免费获得其证明。 组成两种类型，你就有了组成它们证明的材料。

第二步：状态机（一点也不无聊）

事实证明，验证类型只比验证状态难一点 机器和状态机比普通类型有趣得多。这 契约系统使状态转换成为头等大事：

pub struct DbConnected;    // proposition: a connection is open
pub struct QueryExecuted;  // proposition: a query ran successfully
impl Prop for DbConnected {}
impl Prop for QueryExecuted {}

Established 是一个零大小的证明令牌 P 持有。 它只能由实际执行工作的代码构造 编译器随后强制执行转换顺序：您不能调用需要 Established 未先持有 Established.

这是一个经过正式证明的类型安全状态机，证明由以下部分组成。如果 DbConnected 有经过验证的证据 QueryExecuted 有经过验证的证据，他们 连接词 And 也有经过验证的证据，通过 both().

第三步：施工正确的方法（回报）

状态机组成方法。每个证据中保留的主要内容是 一 程序不变量 --系统的一种属性，无论发生什么都能保持不变 执行到那里的路径。

通过在类型系统中表达不变量并在每一步进行验证，开发人员 目标可以投影到类型空间中：定义“准备部署”的含义 一个命题，写下建立其前提条件的函数，以及 编译器保证部署函数只能被调用一次 不变量得到满足。

代理在其中的作用是证明搜索：给定一个目标类型，找到以下序列 将当前状态转换为所需状态的验证操作。每 step是一个具有已知契约的可审计工具调用。由此产生的工具链 *是* 方法——施工正确，事后不核实。

______________________________________________________________________

建筑

该框架有三层：

┌─────────────────────────────────────────────────────────┐
│  Your domain types                                       │
│  #[derive(Elicit)]  →  agent-navigable, MCP-crossing     │
├─────────────────────────────────────────────────────────┤
│  Shadow crates  (elicit_*)                               │
│  Verified vocabularies for third-party libraries         │
│  Types + Methods + Traits = the agent's dictionary       │
├─────────────────────────────────────────────────────────┤
│  Contracts  (Prop / Established
 / And
)           │
│  Postconditions chain into preconditions                 │
│  Workflow correctness enforced at the type level         │
└─────────────────────────────────────────────────────────┘

这三层都由Kani、Creusot和Verus正式验证。

______________________________________________________________________

第1层：你的类型成为原生代理

对于您自己的域名类型， #[derive(Elicit)] 这就是你所需要的。MCP要求所有 跨越边界的值为 Serialize + DeserializeOwned + JsonSchema，所以 你的类型必须派生所有四个类型——编译器可能并不总是能捕获到缺失的impl， 但是如果一个类型没有完全连接，你会得到运行时错误：

use serde::{Serialize, Deserialize};
use schemars::JsonSchema;
use elicitation::Elicit;

// All four derives are required for MCP tool use
#[derive(Debug, Clone, Serialize, Deserialize, JsonSchema, Elicit)]
#[prompt("Configure your deployment")]
#[spec_summary("Deployment configuration with environment and scale settings")]
pub struct DeployConfig {
    #[prompt("Which environment?")]
    pub environment: Environment,   // must also impl Elicitation

    #[prompt("Number of replicas (1–16):")]
    #[spec_requires("replicas >= 1 && replicas  proc_macro2::TokenStream {
    let mut ts = TokenStream::new();
    ts.extend(::kani_proof());
    ts.extend(::kani_proof());
    ts.extend(::kani_proof());
    ts
}

结构体的证明是其部分的并集。添加一个字段，免费获取其证明。

风格系统

每种类型都附带默认提示，但样式系统意味着您永远不会 锁在他们里面。经典用例是 人类与人工智能受众：简洁 机器可读的提示对人类来说是噪音；一个友好的向导风格提示是 对于只需要字段名和约束的代理来说，这同样是浪费。

您不需要实现任何东西——您可以用以下方式注释字段 #[prompt] 和名称 你需要的风格。派生为您生成样式枚举：

#[derive(Debug, Clone, Serialize, Deserialize, JsonSchema, Elicit)]
pub struct DeployConfig {
    // Default prompt (used when no style is active)
    #[prompt("environment")]
    // Named style overrides — derive generates DeployConfigElicitStyle::{ Default, Human, Agent }
    #[prompt("Which environment should we deploy to?", style = "human")]
    #[prompt("environment: production|staging|development", style = "agent")]
    pub environment: Environment,

    #[prompt("replicas")]
    #[prompt("How many replicas? (1–16, default 2):", style = "human")]
    #[prompt("replicas: u8 1..=16", style = "agent")]
    pub replicas: u8,
}

然后在调用站点对每个会话的样式进行热交换——类型不变：

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

// Agent session
let result = DeployConfig::elicit(
    &client.with_style::(DeployConfigElicitStyle::Agent)
).await?;

with_style::(style) 作用于 任何 类型 T 带着一个 Elicitation impl，包括核心crate附带的第三方类型。这是 摆脱供应商锁定：我们的默认提示是一个起点，而不是 约束。

生成器

这 Generator trait是一个简单的契约：给定配置，产生值 目标类型。

pub trait Generator {
    type Target;
    fn generate(&self) -> Self::Target;
}

任何知道如何生成 T 可以实现它——源代码是 完全取决于你。一种传感器融合发生器，用于读取温度和 湿度导出大气压，查找表插值器，物理学 模拟步骤——所有这些都只是“生成 T“，以及 它们与框架中的其他内容组成相同。

struct BarometricGenerator { altitude_m: f32, lapse_rate: f32 }

impl Generator for BarometricGenerator {
    type Target = Pressure;

    fn generate(&self) -> Pressure {
        let p = SEA_LEVEL_PA * (1.0 - self.lapse_rate * self.altitude_m / 288.15).powf(5.2561);
        Pressure::new(p)
    }
}

因为 Generator 这是一个简单的特性，实现可以作为MCP公开 工具通过影子板条箱机器——代理可以请求“生成一个 Pressure 在不知道公式或传感器来源的情况下阅读 模式也适用于代理引发的工作流 *策略* 一次和 程序多次从中驱动生成：

let mode = InstantGenerationMode::elicit(communicator).await?;
let generator = InstantGenerator::new(mode);

let t1 = generator.generate();
let t2 = generator.generate();

这 elicitation_rand crate用 Rand 特征和 #[rand(...)] 与类型编码相同约束的字段属性 形式化证明直接引入抽样策略-- bounded(L, H), positive, nonzero, even, odd，以及 and(A, B) / or(A, B)The 派生生成种子 random_generator(seed: u64) 对于确定性， 可重复输出。 elicitation_rand 运送自己的Kani套件进行验证 发电机履行其申报的合同。

动作特征：启发式语法

每 Elicitation impl基于以下三种之一构建 行动特征 描述 互动范式。这些是所有启发的原始元素 行为被组合起来，并被正式验证：

#[derive(Elicit)] 自动分配正确的动作特征——枚举 单位变体得到 Select, bool 字段得到 Affirm，结构体获取 Survey — 并且导出的状态机相应地对交互进行排序。

连同合同类型(Prop, Established , And )，the 行动特征提供 构造形式验证状态的语法 过渡: Select 将过渡域约束为已知的有限 设置， Affirm 在二进制条件下保护转换，以及 Survey 序列 一组字段转换为单个复合步骤。每个交互都有一个 经核实的证据；交互的组合继承了这些证明。

______________________________________________________________________

第二层：阴影板条箱——特工词典

A. 阴影板条箱 (elicit_*)是第三方库的板条箱形状的词汇表。 它揭示了三件事：

这些共同构成了一个 完整的词汇 为了图书馆。具有访问权限的代理 这三个层都可以推理和组合库的行为，而无需 写一行Rust。

三种工具曝光机制

#[reflect_methods] --对于具有您希望代理调用的方法的新类型：

use elicitation_derive::reflect_methods;

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

#[reflect_trait] --对于第三方特性，其方法值得调用 任何已注册 T: FooTrait:

use elicitation_macros::reflect_trait;

#[reflect_trait(clap::ValueEnum)]
pub trait ValueEnumTools {
    fn value_variants(&self) -> Vec
;
}
// Generates a typed factory: any T: ValueEnum gets value_variants exposed as a tool

碎片工具+ EmitCode --用于无法在MCP上运行的编译时宏 时间（例如。 sqlx::query!, sqlx::migrate!).代理调用一个片段工具 通过以下方式发出经过验证的Rust源代码 EmitCode发出的代码被编译成 宏在实时数据库连接下运行的消费者二进制文件：

#[elicit_tool(
    plugin = "sqlx_frag",
    name   = "query",
    description = "Emit a sqlx::query! call. Establishes: QueryFragmentEmitted.",
    emit_ctx("ctx.db_url" => r#"std::env::var("DATABASE_URL").expect("DATABASE_URL")"#),
)]
async fn emit_query(ctx: Arc
, p: QueryParams) -> Result {
    // p.sql is emitted as a sqlx::query!(p.sql, args...) TokenStream
    // ...
}

可用阴影板条箱

______________________________________________________________________

第三层：契约——类型级别的工作流正确性

合同系统使得在编译时不可能违反工作流先决条件 时间。A. Prop 是一种标记性状； Established 是一个零大小的证明令牌 P 持有； And 编写证明； both() 构造一个连接。

use elicitation::contracts::{Prop, Established, And, both};

// Domain propositions — unit structs that act as type-level facts
pub struct DbConnected;
pub struct QueryExecuted;
impl Prop for DbConnected {}
impl Prop for QueryExecuted {}

// A function that REQUIRES proof of connection
fn fetch_rows(
    sql: &str,
    _pre: Established,   // caller must supply this
) -> Vec {
    // ...
}

// A function that PRODUCES proof of connection
fn connect(url: &str) -> (Pool, Established) {
    let pool = Pool::connect(url);
    (pool, Established::assert())     // assert: we just did the work
}

// Composing proofs
let (pool, db_proof) = connect(&url);
let (_, query_proof) = execute_query(&pool, db_proof);
let both_proof: Established> =
    both(db_proof, query_proof);

影子板条箱运送自己的领域主张。 elicit_sqlx 提供 DbConnected, QueryExecuted, RowsFetched, TransactionOpen, TransactionCommitted, TransactionRolledBack. elicit_reqwest 提供 UrlValid, RequestCompleted, StatusSuccess, Authorized，以及复合材料 FetchSucceeded = And>.

这 Tool trait为可组合的工作流步骤形式化了这种模式：

pub trait Tool {
    type Input: Elicitation;
    type Output;
    type Pre: Prop;
    type Post: Prop;

    async fn execute(
        &self,
        input: Self::Input,
        pre: Established,
    ) -> ElicitResult)>;
}

顺序组成(then)平行组合(both_tools)都是 提供，类型系统强制执行每个步骤 Post 满足 下一步 Pre.

______________________________________________________________________

形式化验证

实现的每种类型 Elicitation 可以携带三个独立的证明 验证者（与 proofs 功能）。默认实现返回空 令牌流；具体实现发出验证源：

// A constrained integer type carrying its own proofs
impl Elicitation for PortNumber {
    // ...elicit(), prompt(), etc...

    #[cfg(feature = "proofs")]
    fn kani_proof() -> proc_macro2::TokenStream {
        quote! {
            #[kani::proof]
            fn verify_port_number_bounds() {
                let n: u16 = kani::any();
                kani::assume(n >= 1024 && n = 1024 && *port  proc_macro2::TokenStream {
        quote! {
            proof fn port_number_invariant(n: u16)
                requires 1024      # Single harness
just verify-creusot   # Creusot
just verify-verus-tracked      # Verus

______________________________________________________________________

能见度

形式证明告诉你什么属性成立。可见性层告诉您 *实际运行的是什么* --并将该信息提供给双方 从静态类型结构到生产，每个级别的开发人员和代理 遥测。

TypeSpec——按需合同

每种启发类型都实现了 ElicitSpec 特质，这是建立起来的 旁边 anodized::spec #[spec] 对其构造函数的注释-- 通过构造保持形式条件和可浏览规范的同步。

TypeSpecPlugin 使用MCP工具显示这些规格 懒惰字典 模式：代理只提取他们需要的规范切片，而不是淹没 带有模式转储的上下文窗口。

类型通过以下方式注册 inventory::submit! 当 #[derive(Elicit)] 是 已使用，因此字典会自动与代码库保持最新状态。

TypeGraph——结构概览

TypeGraphPlugin （特点： graph)呈现以下结构层次 将类型注册为Mermaid图或DOT图——无需阅读源代码。

#[derive(Elicit)] 非泛型类型通过以下方式自动注册 inventory::submit!(TypeGraphKey)。代理人可以打电话 list_types() 到 那么，就发现词汇吧 graph_type("ApplicationConfig") 看看如何 NetworkConfig, Role，以及 DeploymentMode 组成它——一切都在一个 单一工具调用。

启发式内省——无状态可观测性

ElicitIntrospect 是一种延伸的特质 Elicitation 暴露静电 生产仪器的结构元数据：

pub trait ElicitIntrospect: Elicitation {
    fn pattern()  -> ElicitationPattern;  // Survey / Select / Affirm / Primitive
    fn metadata() -> TypeMetadata;        // type_name, description, fields/variants
}

这两种方法都是 零分配的纯函数 --标签的理想选择 无开销的跨度和指标：

// Add type structure to OpenTelemetry / tracing spans
#[tracing::instrument(skip(communicator), fields(
    type_name = %T::metadata().type_name,
    pattern   = %T::pattern().as_str(),
))]
async fn elicit_with_tracing(
    communicator: &impl ElicitCommunicator
) -> ElicitResult {
    T::elicit(communicator).await
}

// Prometheus counter: one metric, labelled by type + pattern
ELICITATION_COUNTER
    .with_label_values(&[T::metadata().type_name, T::pattern().as_str()])
    .inc();

#[derive(Elicit)] 生成 ElicitIntrospect 自动impl， 从构成类型中组合字段和变体元数据。示例 observability_introspection.rs 遍历跟踪、度量、代理 完整的规划和嵌套的内省模式。

______________________________________________________________________

入门指南

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

第一步——推导 Elicit 关于您的域名类型

#[derive(Elicit)] 这就是整个宣言。它生成MCP 往返、模式和 elicit_checked() 方法。在结构体上工作 （调查范式）和枚举（选择范式）相似：

use elicitation::Elicit;
use serde::{Deserialize, Serialize};

/// Finite choice — derives the Select paradigm
#[derive(Debug, Clone, Serialize, Deserialize, Elicit)]
pub enum Difficulty {
    Easy,
    Normal,
    Hard,
}

/// Multi-field form — derives the Survey paradigm  
#[derive(Debug, Clone, Serialize, Deserialize, Elicit)]
pub struct PlayerProfile {
    #[prompt("Enter your name:")]
    pub name: String,
    #[prompt("Pick a difficulty:")]
    pub difficulty: Difficulty,
    pub score: u32,
}

第二步——打电话 elicit_tools! 在你的服务器内部impl

elicitation::elicit_tools! { Type, ... } 在您的内部内联扩展 #[tool_router] impl块。它生成一个交互式 elicit_* 工具 每个列出的类型--没有额外的属性，没有单独的结构：

use elicitation::{ChoiceSet, ElicitServer, Elicitation};
use rmcp::handler::server::wrapper::Parameters;
use rmcp::model::{CallToolResult, Content, ServerCapabilities, ServerInfo};
use rmcp::service::{Peer, RoleServer};
use rmcp::{ErrorData, ServerHandler, tool, tool_handler, tool_router};
use rmcp::handler::server::router::tool::ToolRouter;
use schemars::JsonSchema;
use serde::{Deserialize, Serialize};

#[derive(Debug, Serialize, Deserialize, JsonSchema)]
pub struct StartGameRequest {
    pub session_id: String,
}

pub struct GameServer {
    tool_router: ToolRouter,
}

#[tool_router]
impl GameServer {
    pub fn new() -> Self {
        Self { tool_router: Self::tool_router() }
    }

    /// Regular tool — structured params, no interaction needed
    #[tool(description = "Start a new game session")]
    pub async fn start_game(
        &self,
        Parameters(req): Parameters,
    ) -> Result {
        Ok(CallToolResult::success(vec![
            Content::text(format!("Session {} started", req.session_id)),
        ]))
    }

    /// Interactive tool — gate the LLM inside a walled garden of valid moves
    #[tool(description = "Play a move. You will be prompted to choose a difficulty.")]
    pub async fn play(
        &self,
        peer: Peer,
    ) -> Result {
        // Wrap the peer in ElicitServer to drive the interactive round-trip
        let server = ElicitServer::new(peer);

        // Elicit a free-form struct from the LLM / user
        let profile = PlayerProfile::elicit(&server).await
            .map_err(|e| ErrorData::internal_error(e.to_string(), None))?;

        // Or: constrain to a runtime-computed set of valid options
        let options = vec![1u32, 5, 10, 25];
        let bet = ChoiceSet::new(options)
            .with_prompt("Choose your bet:")
            .elicit(&server)
            .await
            .map_err(|e| ErrorData::internal_error(e.to_string(), None))?;

        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,
    }
}

#[tool_handler(router = self.tool_router)]
impl ServerHandler for GameServer {
    fn get_info(&self) -> ServerInfo {
        ServerInfo::new(ServerCapabilities::builder().enable_tools().build())
    }
}

第三步——发球

#[tokio::main]
async fn main() -> Result> {
    let server = GameServer::new();
    rmcp::service::serve_server(server, rmcp::transport::stdio()).await?;
    Ok(())
}

已注册的工具： start_game, play, elicit_difficulty, elicit_player_profileLLM电话 elicit_difficulty 并返回a 已验证 Difficulty 它可以通过任何地方。 ChoiceSet 把它困在里面 只有运行时允许的选项——围墙花园模式。

添加shadow crate插件

Shadow crates将第三方库作为预构建的工具集公开。添加它们 通过您自己的服务器 PluginRegistry:

use elicitation::PluginRegistry;
use rmcp::ServiceExt;

#[tokio::main]
async fn main() -> Result> {
    PluginRegistry::new()
        .register_flat(GameServer::new())
        .register("http", elicit_reqwest::WorkflowPlugin::default_client())
        .register("db",   elicit_sqlx::SqlxWorkflowPlugin::default())
        .serve(rmcp::transport::stdio())
        .await?;
    Ok(())
}

这暴露了 http__get, db__connect, db__query 与你自己的 工具——一个注册表，一个传输，零粘合代码。

______________________________________________________________________

工作区板条箱地图

______________________________________________________________________

延伸阅读