# 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
```toml
[dependencies]
elicit_sqlx = { version = "0.8" }
rmcp = { version = "0.1", features = ["server"] }
tokio = { version = "1", features = ["full"] }
```
```rust,no_run
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::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`:
```text
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`).
| 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:
| 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:
```rust
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](#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
| [`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):
| [`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):
| [`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.
| `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](#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`.
| `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:
```json
{
"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:
| `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.
```rust
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:
```text
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)`:
```rust
// 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://…`.
| `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
```text
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:
```rust
let full_proof: Established<FullCommit> = full_commit(db_proof, tx_proof, committed_proof);
```
### Example agent workflow
Agent-level (MCP tool calls):
```text
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):
```json
{ "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.