AI导哈

结构化代理交互框架

一个基于形式化验证的结构化代理交互框架，提供类型安全的工具调用、影子库支持和状态机验证。

  • by crumplecup
  • Rust
  • 本地部署
  • 2 星标
  • 更新于
在 GitHub 查看 crumplecup/elicitation

使用说明

引出

由形式验证支持的结构化代理交互。

什么是启发式？

调用您的工具的MCP代理可以以任何顺序传递任何内容。Elicitation颠倒了这一点： 代理不会将任意值推送到您的函数中，您的类型 拉 值从 代理通过验证往返。代理人看到提示；你会得到一个经过验证的、类型安全的 结果。那就是 elicit() 做。

框架的其余部分建立在这个基础之上：

  • 阴影板条箱 为代理提供经过验证的第三方库词汇表
  • 合同 使无效的工作流序列在编译时失败，而不是在运行时失败
  • 已验证状态机 将这三者结合成经过正式验证的程序

每种参与类型都携带三个独立验证器（Kani、Verus、Creusot）的证明， 由其字段自动组成 #[derive(Elicit)].

派生代理本机类型

#[derive(Elicit)] 生成 elicit()，MCP JSON模式，以及通过组合的证明方法 其领域的影响。添加一个字段，免费获取其证明：

#[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? 与代理来回驱动，提示 依次输入每个字段并验证响应。代理不能跳过字段或绕过约束。

交互范式

派生从类型的形状中选择正确的范式：

特质 范式 用于
Select 从有限集合中选择 枚举
Affirm 二进制是/否 bool 田地、警卫台阶
Survey 场激发序列 结构

风格系统

简洁的机器提示对人来说是噪音；友好的向导提示会浪费代理的上下文。 在字段中命名您的受众——派生将生成样式枚举；在呼叫站点交换它：

#[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?;

生成器

Generator<Target> 从任何来源产生目标类型的值——传感器融合， 查找表、物理步骤。 elicitation_rand 添加 #[rand(...)] 字段属性 (bounded(L, H), positive, nonzero, even, odd)并得出一个种子 random_generator(seed: u64) 用于确定性属性测试，拥有自己的Kani套件。

影子板条箱——MCP上常见的API

一个影子箱(elicit_*)使用兼容MCP的类型镜像其源库的API，并且 使用开发人员已经知道的相同名称和类型的工具。目标是让代理工作 随着 elicit_reqwest 感觉就像在工作 reqwest --词汇很熟悉 类型对应，但所有东西都安全地穿过MCP边界。

每个阴影板条箱暴露出三层：

层 它提供了什么 机制
类型 带有源库名称的MCP安全包装器 新类型
方法 作为MCP工具的实例方法 #[reflect_methods]
特质 第三方特征方法作为类型工厂 #[reflect_trait] 
#[reflect_methods]
pub struct ElicitArg(pub clap::Arg);
// Generates: arg__get_long, arg__get_short, arg__get_help, ... as MCP tools

对于编译时宏（例如。 sqlx::query!)，片段工具通过以下方式发出经过验证的Rust源代码 EmitCode；宏在消费者二进制文件中扩展，其中有实时连接可用。

域 阴影板条箱
Web/HTTP elicit_reqwest, elicit_axum, elicit_tower
数据库 elicit_sqlx, elicit_redb, elicit_db
异步运行时 elicit_tokio
CLI elicit_clap
用户界面/图形 elicit_egui, elicit_ratatui, elicit_bevy, elicit_wgpu, elicit_winit, elicit_accesskit, elicit_leptos, elicit_ui
GIS/几何 elicit_geo, elicit_geo_types, elicit_geojson, elicit_georaster, elicit_gis, elicit_proj, elicit_rstar, elicit_wkb, elicit_wkt
日期/时间 elicit_chrono, elicit_jiff, elicit_time
数据格式 elicit_csv, elicit_serde, elicit_serde_json, elicit_toml
字符串/类型实用程序 elicit_url, elicit_regex, elicit_uuid, elicit_uom, elicit_std

契约——作为类型的不变量

程序具有不受执行路径影响的不变量。大多数框架将其保留为 注释或运行时检查——开发人员知道但编译器不知道的东西 它们在类型系统中是明确的。

A. Prop 是一种标记类型：不变量的名称。 Established<P> 是一个零大小的证明 象征着 P 它之所以存在，是因为某种东西产生了它，也是产生它的唯一途径 它是通过a ProvableFrom 交换：

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

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

交换存在于一种特质方法中——而这种特质方法就是 唯一的门 到令牌：

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
}

因为trait方法是唯一的构造函数 Established<QueryValidated>，业务 逻辑 必须 跑。编译器强制执行它。然后，证明可以验证这个链是健全的。

And<P,Q> 编写证明； both(p, q) 构造连词。影子板条箱自己装运 Prop 类型： elicit_sqlx 有 DbConnected, QueryExecuted, TransactionOpen; elicit_reqwest 有 UrlValid, RequestCompleted, FetchSucceeded.

已验证状态机

验证状态机是每个状态都实现的状态机 Elicitation 和 每一次转变都是 #[formal_method]这种双重约束正是导数所需要的 自动生成证明：所有输入和输出都在经过验证的类型系统内，并且所有 转换遵循 ProvableFrom 合同——所以没有通过机器的路径 框架无法检查和验证。

// 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] 大门 #[instrument] 所以证明工具链不会追逐追踪内部， 并记录线束生成的转换。生成的证明验证了每个 可达转换保留了一致性谓词——构造的正确性。

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

形式化验证

证明基础设施是自下而上的。地心末日 elicitation 板条箱船验证证明 特性门后面的stdlib和第三方类型——捕获有意义的边界：a PortNumber 总是在[10246535]；一 NonEmptyString 长度总是大于0；一 Established<FetchSucceeded> 总是由2xx响应产生。当你推导 Elicit 根据你自己的类型，你的证明是由这些规范证明组成的。结构体的证明是 其字段证明的联合——添加一个字段，免费获得其验证边界。

在VSM级别，证明验证了更丰富的声明：每个转换都保留了 一致性谓词。三个验证者从独立的方向进行验证：

验证器 方法 当前工作区覆盖率
卡尼 有界模型检查——详尽的有界内 388个传递线束
维鲁斯 基于SMT的程序逻辑 158个通过证明
克勒索 演绎验证——丰富的组合不变量 22837个有效目标/19个模块 
just verify-kani-tracked
just verify-creusot <file.rs>
just verify-verus-tracked

能见度

使用不熟悉代码库的代理无法读取源代码。三个特征揭示了 在运行时使用词汇表，而不会淹没上下文窗口：

类型规格 表面 ElicitSpec 注释作为MCP工具。 describe_type 返回a 可用类别的摘要和列表； explore_type 返回一个类别-- requires, ensures, bounds, fields --根据需求。特工只提取他们需要的东西。

TypeGraph 将注册类型的结构层次呈现为Mermaid或DOT图。 list_types() → graph_type("ApplicationConfig") 显示如何 NetworkConfig, Role，以及 DeploymentMode 在一次工具调用中编写它。

启发式反思 公开零分配 pattern() 和 metadata() 用于标签 跟踪跨度和Prometheus指标——无需源解析，无需分配：

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

#[derive(Elicit)] 为所有三个过孔注册类型 inventory::submit! 自动。

入门指南

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

推导 Elicit 关于您的域名类型，请致电 elicit() 在工具处理程序内部，并公开 通过 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 }
}

通过以下方式在您自己的服务器旁边添加shadow crate插件 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?;

一个注册表，一个传输，零胶水代码。

工作区板条箱地图

板条箱 角色
elicitation 核心：特征、合同、MCP管道
elicitation_derive Proc宏： #[derive(Elicit)], #[formal_method], #[reflect_methods], #[reflect_trait]
elicitation_rand 随机值生成
elicit_proofs 生成的线束（Kani/Verus/Creusot）
elicitation_kani / elicitation_creusot 证明库和支持
elicit_server MCP服务器支持
elicit_clap CLI词汇表（规范的shadow crate参考）
elicit_* 30+域影子箱--请参阅 阴影板条箱 上面

进一步阅读

文档 主题
SHADOW_CRATE_MOTIVATION.md 倒置论
THIRD_PARTY_SUPPORT_GUIDE.md 添加新的阴影板条箱
ELICITATION_WORKFLOW_ARCHITECTURE.md 工作流基础架构
CREUSOT_GUIDE.md Creusot注释图案
FORMAL_VERIFICATION_LEGOS.md 成分证明策略
crates/elicit_clap/ 标准参考阴影箱

相关 MCP