Skip to content

v0.9.0 — Real Proof Emission & Cross-Crate Verified Workflows

Choose a tag to compare

View all tags
@crumplecup crumplecup released this 06 Mar 02:21
· 880 commits to main since this release
v0.9.0
8787456

v0.9.0 — Real Proof Emission & Cross-Crate Verified Workflows

This is a breaking release. The formal verification proof methods now return real, executable proof code instead of tautological stubs.

Breaking: proof emission redesigned

kani_proof(), verus_proof(), creusot_proof(), and prusti_proof() on the Elicitation trait no longer return (). They now return proc_macro2::TokenStream containing real, runnable proof harnesses.

Before:

#[cfg(kani)]
fn kani_proof() { assert!(true, "placeholder"); }

After:

fn kani_proof() -> proc_macro2::TokenStream {
    quote! {
        #[kani::proof]
        fn verify_u8_positive_is_nonzero() {
            let v: u8 = kani::any();
            kani::assume(v > 0);
            assert!(v != 0);
        }
    }
}

172 tautological void stubs have been removed. The derive macro now aggregates sub-proofs from struct/enum fields recursively, so a derived type emits a composite proof that covers all its constituents. proc_macro2 and quote are now core deps activated unconditionally (a proof-emission feature gate to make them optional is planned for v0.9.1).

New shadow crates

Five new shadow crates bring datetime and URL types into the elicitation ecosystem with full MCP tool sets, verified workflows, and type-level contracts:

Crate Wraps Tools
elicit_chrono chrono::DateTime<Utc/Fixed>, NaiveDateTime year, month, day, hour, offset, to_rfc3339, compute_duration, …
elicit_url url::Url scheme, host, port, path, query, join, origin, …
elicit_jiff jiff::Timestamp, jiff::Zoned timestamp arithmetic, timezone-aware ops, …
elicit_time time::OffsetDateTime, PrimitiveDateTime RFC 3339 parse, offset ops, add_seconds, …
elicit_regex regex::Regex is_match, find, find_all, replace_all, captures_len

Each crate bridges a third-party type that lacked Serialize/Deserialize/JsonSchema support, making it usable in #[derive(Elicit)] structs.

elicit_server: cross-crate verified workflows

elicit_server is the new home for compositions that span multiple crates. Individual shadow crates prove local invariants; elicit_server chains them into end-to-end contracts the compiler enforces structurally:

SecureFetchPlugin (elicit_url + elicit_reqwest)

UnvalidatedUrl → UrlParsed → HttpsRequired → RequestCompleted ∧ StatusSuccess

An agent cannot reach RequestCompleted without first passing through HttpsRequired. HTTPS enforcement is not a runtime check — it is unreachable to bypass.

FetchAndParsePlugin (elicit_reqwest + elicit_serde_json)

RequestCompleted → JsonParsed → PointerResolved

The JSON pointer is only resolvable against a value that was provably fetched and parsed. The agent builds the proof chain step by step.

With the emit feature, EmitBinaryPlugin recovers an agent's verified interactive session as a standalone, compilable Rust binary — typestate ceremony, proof tokens, and all.

Test coverage

  • 39 smoke tests covering all crates and cross-crate workflow plugins
  • Third-party MCP compat coverage matrix added (elicitation/tests/third_party_mcp_compat_test.rs)
  • Workspace dependency inheritance normalised (workspace = true across all shadow crates)

Upgrading

If your code calls kani_proof(), verus_proof(), creusot_proof(), or prusti_proof() and discards the return value, it will continue to compile. If you pattern-matched on (), update to handle proc_macro2::TokenStream.

Assets 2
Loading