elicit_sqlx

MCP-enabled database workflows built on [sqlx], [elicitation], and [rmcp].

Wraps sqlx's Any-driver types as MCP tools and fragment emitters, giving an agent a complete vocabulary for constructing verified database workflows without writing any Rust by hand.

---

What this crate provides

Four complementary layers:

1. Newtype wrappers — serde + JsonSchema-enabled newtypes for sqlx types that lack those impls, so database values can cross the MCP boundary
2. Any-driver runtime tools — five SqlxPlugin tools that execute SQL against a real database via the Any driver and return structured results
3. Driver-specific plugins — three plugins (SqlxPgPlugin, SqlxSqlitePlugin, SqlxMySqlPlugin) that expose stateful, UUID-keyed connection pools and transactions for Postgres, SQLite, and MySQL respectively
4. Fragment tools — four SqlxFragPlugin tools that emit Rust source wrapping sqlx's compile-time macros (query!, query_as!, query_scalar!, migrate!)

---

Quick start

[dependencies]
elicit_sqlx = { version = "0.8" }
rmcp = { version = "0.1", features = ["server"] }
tokio = { version = "1", features = ["full"] }

use elicitation::PluginRegistry;
use elicit_sqlx::{SqlxPlugin, SqlxFragPlugin, SqlxPgPlugin, SqlxSqlitePlugin};

let registry = PluginRegistry::new()
    .register("sqlx",      SqlxPlugin::default())
    .register("sqlx_frag", SqlxFragPlugin)
    .register("pg",        SqlxPgPlugin::new())
    .register("sqlite",    SqlxSqlitePlugin::new());

// Any-driver tools: sqlx__fetch_all, sqlx_frag__query, …
// Postgres tools:   pg__connect, pg__begin, pg__tx_execute, pg__commit, …
// SQLite tools:     sqlite__connect, sqlite__execute, sqlite__fetch_all, …

---

How elicit_sqlx satisfies the shadow crate motivation

The shadow crate motivation is stated in SHADOW_CRATE_MOTIVATION.md. The core idea is:

Define a vocabulary of atomic, verified operations — let an agent compose them into tool chains — the tool chain is the method.

Database access is one of the hardest domains to verify after the fact: queries are strings, result shapes are dynamic, and the type system of the application rarely reflects the schema it reads from. elicit_sqlx attacks this from the vocabulary end: by making every sqlx operation an explicitly typed, MCP-callable tool with a machine-checkable contract, agent-composed database workflows inherit those contracts structurally rather than requiring per-method proofs.

The Any driver as the verification bridge

sqlx is generic over database backends (Postgres, Sqlite, MySql, …). Its compile-time generics are powerful but opaque at the MCP boundary — you cannot pass sqlx::Row<Postgres> over JSON. sqlx solves this with the Any driver: a runtime-erased backend that unifies all supported databases behind a single concrete type family.

sqlx Any type	Role in elicit_sqlx
sqlx::any::AnyRow	Query result transport across the MCP boundary
sqlx::any::AnyColumn	Column metadata (name, ordinal, type)
sqlx::any::AnyTypeInfo	SQL type descriptor
sqlx::any::AnyQueryResult	DML result (rows affected, last insert ID)
sqlx::any::AnyPool	Connection pool held in SqlxContext
sqlx::Error	Error introspection

The Any types are the bridge: they are concrete enough to serialize and schema- describe, yet backend-agnostic enough to work with any sqlx-supported database. An agent that learns the Any vocabulary has a verified dialect that works with Postgres, SQLite, and MySQL without any driver-specific knowledge.

SqlTypeKind — the type vocabulary for SQL

The key connection between the Any type family and formal verification is AnyTypeInfoKind, sqlx's enum of known SQL type variants. We surfaced this as SqlTypeKind in the elicitation crate (a Select enum with Elicitation derived), giving it three things sqlx itself does not provide:

• JsonSchema — so it can appear in MCP tool parameter and return schemas
• serde — so values can cross the MCP boundary
• Kani/Creusot/Verus proofs — so an agent can reason about which type kinds are valid, how many variants exist, and which labels round-trip

When an agent calls any_column__type_kind() and receives SqlTypeKind::Text, it is receiving a formally verified, schema-described value — not a raw string — that it can use to drive the next step in its tool chain.

---

Type choices: what we shadowed and why

AnyRow — the central result type

sqlx::any::AnyRow is not Clone, not Serialize, and not JsonSchema. It also holds internal Arc state that must survive cloning across async boundaries. We could not use elicit_newtype! here, so AnyRow is hand- written with:

• Arc<sqlx::any::AnyRow> as the inner field (cheap clone across tool calls)
• Manual JsonSchema and Debug impls
• #[reflect_methods] on six methods: columns(), len(), is_empty(), column_names(), columns_as_descriptors(), and to_row_data()

The key method is to_row_data(), which materialises the row into a RowData — a fully serializable owned snapshot that crosses the MCP boundary cleanly. This is the exit point from sqlx's world into the agent's world.

RowData holds Vec<ColumnEntry>, and each ColumnEntry carries a ColumnValue — our own enum that mirrors AnyValueKind:

AnyValueKind (sqlx, non_exhaustive, non-Serialize)
    ↓  decode_val()
ColumnValue (ours, Serialize + JsonSchema + verified)
    ↓  ColumnEntry
RowData (fully serializable row snapshot)

decode_val() matches directly on AnyValueKind variants rather than going through the Decode trait. This avoids type-dispatch overhead and correctly handles null values, which sqlx encodes as AnyValueKind::Null(kind) (a null with a type annotation) rather than a failed decode. The match arm is marked with a wildcard fallback because AnyValueKind is #[non_exhaustive] — new sqlx variants fall through to ColumnValue::Null rather than breaking builds.

AnyColumn — column metadata

sqlx_core::any::AnyColumn is the type backing column descriptors in every row. It implements sqlx::Column and sqlx::TypeInfo but not serde or JsonSchema. We wrap it with elicit_newtype! and expose four methods: ordinal(), name(), type_kind(), and type_name().

One note on the import path: AnyColumn is internally a sqlx_core type re-exported through several levels of sqlx's module hierarchy. We import it directly from sqlx_core::any::AnyColumn to avoid ambiguity with the outer sqlx::Column trait of the same name.

AnyTypeInfo — SQL type descriptor

Wraps sqlx::any::AnyTypeInfo with elicit_newtype! and exposes kind(), name(), and is_null(). The kind() method returns a SqlTypeKind, completing the chain from raw database type information to a formally verified Select enum value.

AnyQueryResult — DML results

sqlx::any::AnyQueryResult holds two public fields: rows_affected: u64 and last_insert_id: Option<i64>. It does not implement Serialize, so we wrap it with elicit_newtype! for method reflection and add QueryResultData — a plain serializable struct carrying those same two fields — as the MCP- boundary transport type.

SqlxError — error introspection

sqlx::Error is a large non-serializable enum. We wrap it with elicit_newtype! and expose two methods: kind_label() (returns a string label for the variant, e.g. "Database", "RowNotFound") and message() (full display string). This lets agents diagnose errors without receiving an opaque error blob.

SqlxContext — connection pool carrier

SqlxContext wraps AnyPool and implements PluginContext. It is the connection-pool carrier in stateful workflows where the same pool should persist across multiple tool calls. The top-level connect() function installs the Any driver and produces a context from a database URL.

---

Driver-specific plugins

Pool<Db> and Connection<Db> are generic over the driver type, which makes them opaque to MCP tool schemas. The solution is monomorphization: rather than trying to express the generic, we shadow the concrete type aliases that actually appear in user code — PgPool, SqlitePool, MySqlPool — and generate a full stateful plugin for each one via the impl_driver_plugin! macro.

Each driver plugin (SqlxPgPlugin, SqlxSqlitePlugin, SqlxMySqlPlugin) holds:

• Arc<Mutex<HashMap<Uuid, Pool>>> — named persistent pools
• Arc<Mutex<HashMap<Uuid, Transaction<'static, Db>>>> — open transactions

Pools are Clone (Arc-backed), so the lock is released before any async call. Transactions are !Clone, so they are removed from the registry, used, and re-inserted — ensuring the lock is never held across an await point.

The 14-tool surface

All tool names follow the pattern {prefix}__{verb}, where the prefix is chosen at registration time (e.g. pg, sqlite, mysql).

Category	Tool	Description
Pool	*__connect	Establish pool from URL; returns ConnectResult { pool_id }
Pool	*__disconnect	Remove and close a named pool
Pool	*__pool_stats	Returns { size, num_idle, is_closed }
Direct	*__execute	Execute non-returning SQL; returns QueryResultData
Direct	*__fetch_all	SELECT returning all rows as Vec<RowData>
Direct	*__fetch_one	SELECT returning first row; errors if none
Direct	*__fetch_optional	SELECT returning first row or null
Transaction	*__begin	Begin transaction; returns BeginResult { tx_id }
Transaction	*__commit	Commit and remove a transaction
Transaction	*__rollback	Roll back and remove a transaction
Tx SQL	*__tx_execute	Execute non-returning SQL inside a transaction
Tx SQL	*__tx_fetch_all	SELECT inside a transaction
Tx SQL	*__tx_fetch_one	SELECT one row inside a transaction
Tx SQL	*__tx_fetch_optional	SELECT optional row inside a transaction

Why not the Any driver here?

SqlxPlugin uses AnyPool, which works with any backend but requires sqlx::any::install_default_drivers() at runtime and routes through a dynamic dispatch layer. Driver-specific plugins bypass that layer, using the native PgPool/SqlitePool/MySqlPool API directly. This also gives access to driver-specific result data — for example:

Driver	last_insert_id
Postgres	None (use RETURNING id in your SQL)
SQLite	last_insert_rowid() → i64
MySQL	last_insert_id() → u64 (cast to i64)

Each driver's row decoder dispatches on TypeInfo::name() strings appropriate for that engine rather than the AnyValueKind enum.

DriverKind — the verification bridge for drivers

The DriverKind Select enum in the elicitation crate (under the sqlx-types feature) names the three supported drivers with full Kani, Creusot, and Verus coverage:

use elicitation::DriverKind;

let k = DriverKind::Postgres;
assert_eq!(k.url_scheme(), "postgres");
assert_eq!(k.feature_name(), "postgres");

Formally verified properties:

• Label count equals option count (3 variants, de-trusted in Creusot)
• Known labels round-trip through from_label()
• Unknown labels return None

---

What we chose not to shadow, and why

Generic Pool<Db> and Connection<Db> as open generics

The generic forms (Pool<Postgres>, Pool<Sqlite>, etc.) cannot appear in MCP tool schemas without a concrete type argument — and that argument belongs to the user's binary, invisible to the MCP server. We solve this through two paths:

• AnyPool (SqlxPlugin) — erases the driver at runtime; one tool set covers all backends.
• Monomorphized plugins (SqlxPgPlugin, SqlxSqlitePlugin, SqlxMySqlPlugin) — each shadows the concrete type alias for one backend, giving full stateful pool and transaction support with driver-specific fidelity.

The open generic Pool<DB> itself is never surfaced at the MCP boundary.

Query<'q, DB, Args> and the typed query family

sqlx's query(), query_as(), and query_scalar() return builder types generic over lifetime, database, and argument list. These cannot be serialized or passed as tool arguments. We solve this in two complementary ways:

1. Runtime tools (SqlxPlugin) — accept a raw { database_url, sql } pair and execute immediately, returning serializable results. The builder state lives only in the tool implementation, never at the MCP boundary.
2. Fragment tools (SqlxFragPlugin) — emit Rust source code wrapping the compile-time macros (query!, query_as!, etc.) for inclusion in user binaries. This is the correct solution for code paths that need compile-time query verification; the agent composes the fragment and hands it to std__assemble.

Positional SQL arguments are handled separately — see Parameterized queries below.

PgArguments and the Encode wall

PgArguments::add<T: Encode> is generic — the Encode bound is monomorphic at compile time. elicit_newtype! and #[reflect_methods] cannot reflect generic methods across the MCP boundary, so we cannot shadow PgArguments directly.

Instead we provide two complementary mechanisms:

• Inline JSON args — pass args: [v1, v2, …] directly on any driver plugin tool. JSON values are converted to native driver bindings at dispatch time.
• ToSqlxArgsFactory — for user types that deserve schema-accurate tooling, prime_to_sqlx_args::<T>() registers a {prefix}__to_sqlx_args tool that converts the full JSON-serialized T into an ordered arg vector. The output can be passed directly as args to any execute/fetch tool.

sqlx::Row as a trait object

The Row trait is object-unsafe (it is generic over the column accessor), so Box<dyn Row> does not exist. We work entirely with the concrete AnyRow type, which is what all Any-driver queries return.

Migrate and Migrator

sqlx's migration types do their real work at compile time (via migrate!). We expose migration as a fragment tool (sqlx__migrate) that emits the correct sqlx::migrate! invocation for assembly into a binary. Runtime-only migration workflows can also use the execute tool directly.

---

Newtype wrappers

Wrapper	Inner type	Construction	Notes
[AnyRow]	sqlx::any::AnyRow	Hand-written (Arc)	Non-Clone inner; to_row_data() is the MCP exit
[AnyColumn]	sqlx_core::any::AnyColumn	elicit_newtype!	Imported from sqlx_core directly
[AnyTypeInfo]	sqlx::any::AnyTypeInfo	elicit_newtype!	kind() returns SqlTypeKind
[AnyQueryResult]	sqlx::any::AnyQueryResult	elicit_newtype!	to_result_data() for MCP transport
[SqlxError]	sqlx::Error	elicit_newtype!	kind_label() + message() for diagnosis

Transport types (fully serializable, live at the MCP boundary):

Type	Description
[RowData]	Owned row snapshot: Vec<ColumnEntry>
[ColumnEntry]	Column name + ColumnValue
[ColumnValue]	Serializable mirror of AnyValueKind
[ColumnDescriptor]	Column name, ordinal, and SqlTypeKind
[QueryResultData]	rows_affected + last_insert_id

Select enums (formally verified via Kani/Creusot/Verus):

Enum	Source	Variants
[SqlTypeKind]	elicitation::SqlTypeKind	Maps AnyTypeInfoKind
[ErrorKind] (in elicitation)	sqlx::error::ErrorKind	Maps sqlx error categories
[DriverKind] (in elicitation)	elicitation::DriverKind	Postgres, Sqlite, MySql

---

Any-driver runtime tools (SqlxPlugin)

All five tools accept { database_url, sql? } and open a short-lived pool per call — no persistent connection state is required. These use the Any driver, so one tool set works against Postgres, SQLite, and MySQL alike.

Tool	Description
sqlx__connect_check	Verify a URL is reachable
sqlx__execute	Execute a non-returning statement; returns QueryResultData
sqlx__fetch_all	SELECT returning all rows as Vec<RowData>
sqlx__fetch_one	SELECT returning first row; errors if none found
sqlx__fetch_optional	SELECT returning first row or null

For persistent pools, transaction support, or driver-specific result data, use the driver-specific plugins instead.

---

Fragment tools (SqlxFragPlugin)

Fragment tools emit Rust source code for sqlx compile-time macros. They do not execute SQL — they return source fragments for the agent to assemble into a binary via std__assemble.

Tool	Emits	Notes
sqlx_frag__query	sqlx::query!(sql, params…)	Requires DATABASE_URL at compile time
sqlx_frag__query_as	sqlx::query_as!(Type, sql, params…)	Target type must impl sqlx::FromRow
sqlx_frag__query_scalar	sqlx::query_scalar!(sql, params…)	Returns a single scalar
sqlx_frag__migrate	sqlx::migrate!("path") + .run(&pool)	Path is relative to crate root

The fragment pattern handles the fundamental tension in sqlx's design: its most powerful feature (compile-time query verification against a live schema) requires the user's binary to be compiled with DATABASE_URL set — something that cannot happen inside the MCP server process. Fragment emission sidesteps this: the agent composes the verified macro call, and the user's binary carries out the compile-time check.

---

Parameterized queries

All driver plugin tools accept an optional args field for positional SQL parameters. When present, the tool uses sqlx::query_with(sql, bindings) instead of bare sqlx::query(sql).

Inline JSON args

Pass values directly as a JSON array:

{
  "pool_id": "…",
  "sql": "INSERT INTO users (name, age) VALUES ($1, $2)",
  "args": ["Alice", 30]
}

JSON values are converted to native driver bindings at dispatch time:

JSON value	Binding
true / false	bool
integer number	i64
floating-point number	f64
string	String
null	Option::<String>::None

ToSqlxArgsFactory — typed arg conversion

For user types that need schema-accurate tool input, register the type with the ToSqlxArgsFactory. For each registered T, a {prefix}__to_sqlx_args tool is contributed with T's full JSON Schema as its input schema.

prime_to_sqlx_args::<CreateUser>();
registry.register_type::<CreateUser>("create_user");
// Agent can now call: create_user__to_sqlx_args { target: { … } }

Three-step agent workflow:

1. pg__connect { url }
       → { pool_id: "abc" }

2. create_user__to_sqlx_args { target: { name: "Alice", age: 30 } }
       → { result: ["Alice", 30] }

3. pg__execute { pool_id: "abc",
                 sql: "INSERT INTO users(name,age) VALUES($1,$2)",
                 args: ["Alice", 30] }
       → { rows_affected: 1 }

Field values are emitted in struct declaration order (serde_json preserves insertion order via IndexMap), so positional parameter alignment is reliable.

Non-object JSON (e.g. a newtype wrapping a scalar) is wrapped in a single-element Vec, which works naturally with single-parameter queries.

---

Verified workflows (SqlxWorkflowPlugin)

The driver-specific plugins provide the letters of the alphabet (connect, execute, fetch). SqlxWorkflowPlugin arranges them into words — complete, contract-carrying workflows where each step proves it did what it claimed.

Propositions

Each tool establishes a proposition — a zero-sized PhantomData proof marker that documents what the tool guarantees:

Proposition	Meaning
DbConnected	A named pool was successfully opened
QueryExecuted	A SQL statement completed and rows_affected is known
RowsFetched	A SELECT returned ≥0 rows
TransactionOpen	A transaction was started and is not yet resolved
TransactionCommitted	A transaction was committed
TransactionRolledBack	A transaction was rolled back

Propositions compose with And<P,Q> and both(p, q):

// Type aliases for common chains
pub type ConnectedAndExecuted = And<DbConnected, QueryExecuted>;
pub type FullCommit = And<DbConnected, And<TransactionOpen, TransactionCommitted>>;

// Combinator functions
pub fn connected_and_executed(
    db: Established<DbConnected>,
    qe: Established<QueryExecuted>,
) -> Established<ConnectedAndExecuted>

pub fn full_commit(
    db: Established<DbConnected>,
    tx: Established<TransactionOpen>,
    committed: Established<TransactionCommitted>,
) -> Established<FullCommit>

All proposition types and combinators are zero-sized — they vanish at compile time. An Established<P> costs nothing at runtime.

The 13-tool verified surface

SqlxWorkflowPlugin uses AnyPool (driver-agnostic) so one plugin covers all three drivers. The URL determines the backend: postgres://…, sqlite:…, mysql://….

Tool	Establishes	Description
sqlx_workflow__connect	DbConnected	Open pool, return pool_id
sqlx_workflow__disconnect	—	Close and remove pool
sqlx_workflow__execute	QueryExecuted	SQL + args → QueryResultData
sqlx_workflow__fetch_all	RowsFetched	SELECT → Vec<RowData>
sqlx_workflow__fetch_one	RowsFetched	SELECT → first RowData
sqlx_workflow__fetch_optional	—	SELECT → Option<RowData>
sqlx_workflow__begin	TransactionOpen	Start transaction → tx_id
sqlx_workflow__commit	TransactionCommitted	Commit transaction
sqlx_workflow__rollback	TransactionRolledBack	Rollback transaction
sqlx_workflow__tx_execute	QueryExecuted	SQL within transaction
sqlx_workflow__tx_fetch_all	RowsFetched	SELECT within transaction
sqlx_workflow__tx_fetch_one	RowsFetched	SELECT (first) within transaction
sqlx_workflow__tx_fetch_optional	—	SELECT (optional) within transaction

Contract chain diagram

connect(url)
  └─ Established<DbConnected>           pool_id: Uuid

execute(pool_id, sql, args)
  └─ Established<QueryExecuted>         QueryResultData { rows_affected, last_insert_id }

fetch_all(pool_id, sql, args)
  └─ Established<RowsFetched>           Vec<RowData>

begin(pool_id)
  └─ Established<TransactionOpen>       tx_id: Uuid

tx_execute(tx_id, sql, args)
  └─ Established<QueryExecuted>

commit(tx_id)
  └─ Established<TransactionCommitted>

rollback(tx_id)
  └─ Established<TransactionRolledBack>

Full proof of a committed transaction:

let full_proof: Established<FullCommit> = full_commit(db_proof, tx_proof, committed_proof);

Example agent workflow

Agent-level (MCP tool calls):

1. sqlx_workflow__connect { database_url: "sqlite::memory:", max_connections: 1 }
   → { pool_id: "a1b2…" }          — DbConnected established

2. sqlx_workflow__execute { pool_id: "a1b2…", sql: "CREATE TABLE …", args: [] }
   → { rows_affected: 0 }           — QueryExecuted established

3. sqlx_workflow__begin { pool_id: "a1b2…" }
   → { tx_id: "c3d4…" }            — TransactionOpen established

4. sqlx_workflow__tx_execute { tx_id: "c3d4…", sql: "INSERT …", args: [42] }
   → { rows_affected: 1 }           — QueryExecuted established within tx

5. sqlx_workflow__commit { tx_id: "c3d4…" }
   → {}                             — TransactionCommitted established

6. sqlx_workflow__disconnect { pool_id: "a1b2…" }

sqlite::memory: note

SQLite's :memory: backend creates a separate database per connection. When using a pool, pass max_connections: 1 to ensure all operations share one connection (and one in-memory database):

{ "database_url": "sqlite::memory:", "max_connections": 1 }

For Postgres and MySQL, max_connections defaults to the sqlx default (10).

---

All sqlx Select enum types in the elicitation crate have Kani, Creusot, and Verus proofs covering:

• Label count — labels().len() == options().len() (de-trusted in Creusot via extern_spec! axioms in elicitation_creusot/extern_specs.rs)
• Roundtrip — every label returned by labels() is accepted by from_label()
• Rejection — from_label("__unknown__") returns None

The ColumnValue and RowData transport types have Verus proofs on their constructors, and AnyQueryResult's field accessors are covered by Kani harnesses.

The ToSqlxArgs dispatch logic has three Kani harnesses (verify_to_sqlx_args_null_is_single_element, verify_to_sqlx_args_bool_is_single_element, verify_to_sqlx_args_object_extracts_values), two Creusot proofs, and three Verus structural contracts covering the null, bool, and object dispatch arms.

The SqlxWorkflowPlugin proposition combinators have three Kani harnesses, two Creusot proofs, and three Verus structural contracts proving that Established<P>, And<P,Q>, and both() are all zero-sized (compile-time only, zero runtime cost).

See FORMAL_VERIFICATION_LEGOS.md for the compositional proof strategy.