Amenable

A declarative interface amenable to formal verification.

---

What is Amenable?

Software that claims to be "verified" is usually trusted on faith: a comment says so, a test suite is green, and a reviewer has no way to check what was actually established or how much confidence it deserves. amenable makes that distinction explicit and load-bearing. It is the foundational, dependency-light trait family for lawful proof-carrying software structure: it defines the roles and admissibility criteria governing a proof economy — which types are permitted to serve as trusted roots, which types may count as derived evidence, which exchanges are lawful, and which workflows are closed under those exchanges.

Every claim in the system is backed by exactly one of two lawful things — never a silent third option:

• a genuine machine-checked proof, emitted through Witness and consumed by a Verifier backend (Kani, Creusot, Verus)
• an explicit Standard or Objective certification of provenance — a structured, auditable record naming the authority, source, and rationale for a trust decision that cannot be mathematically derived

Three independent verifier backends implement Witness against the same carriers, so a claim proven under Kani and Creusot and Verus independently is much stronger evidence than any one alone — and the registry backing all of this is queryable at any time, not just documentation (see Try it below).

amenable is upstream of every framework that consumes it. Formal verification does not depend on any downstream conversational or domain framework; those frameworks depend on amenable.

See amenable.md for the trait-by-trait design and docs/AMENABLE_PLAN.md for the original architectural rationale this project was built from. Planning documents for individual features live in docs/, indexed by docs/PLANNING_INDEX.md.

Try it

amenable::proof_chain looks up a registered evidence chain and returns an auditable report — the same thing the amenable audit CLI subcommand prints. This is a real, tested example (crates/amenable/examples/audit_proof_chain.rs), runnable as-is:

fn main() -> Result<(), amenable::ChainError> {
    let report = amenable::proof_chain("RustStdStandard<char>")?;
    println!("{report}");
    Ok(())
}

$ cargo run --example audit_proof_chain
Proof chain for amenable_std::rust_std::RustStdStandard<char> (complete for: kani)

amenable_std::rust_std::RustStdStandard<char> (root)
  proof [kani]:
    harness: verify_char_unicode_scalar
    claim: /// `char` is constrained to Unicode scalar values (excludes the
            /// surrogate range `0xD800..=0xDFFF`) and round-trips through `u32`.
            #[kani::proof]
            fn verify_char_unicode_scalar() {
                let c: char = kani::any();
                let u = c as u32;

                assert!(
                    u <= 0xD7FF || (0xE000..=0x10FFFF).contains(&u),
                    "char is a valid Unicode scalar value"
                );

                let c2 = char::from_u32(u).expect("valid unicode scalar round-trips");
                assert!(c == c2, "char round-trips through u32");
            }
    rust.authority_kind: external_standard
    rust.authority: Rust Project Developers
    rust.source_crate: core
    rust.source_module: core::primitive
    source_url: https://doc.rust-lang.org/std/primitive.char.html
    type_name: char
    semantic_summary: The character carrier stores a Unicode scalar value.

That's the whole story in miniature: the claim ("char is a valid Unicode scalar value and round-trips through u32") is backed by the actual Kani proof source, not a description of one, and the report says explicitly which verifiers it's complete for. Build with --features creusot,verus and the same lookup returns all three independent proofs for this claim, not just Kani's.

The amenable CLI wraps this and more:

• amenable audit — write the registered proof chain for one evidence name (what the example above does)
• amenable assess — record and report structured, reviewer-owned assessments of registered proof harnesses
• amenable gallery — run and inspect non-production Kani proof-gallery experiments
• amenable dump-registry — write the full evidence and proof registry as JSON
• amenable verify — run registered proof harnesses through a verifier backend

Run amenable --help (or amenable <subcommand> --help) for the full option set.

Workspace

Crate	Role
amenable	Top-level facade + the CLI above
amenable_core	The constitutional trait family itself — Verifier, Witness, Evidence, Standard, Sidecar, Establish, Exchange, StateMachine, Provenance
amenable_derive	Proc macros the trait family needs (harness!, #[derive(Provenance)], #[calculation], ...)
amenable_std	RustStdType + the registry where all three verifiers' witnesses converge
amenable_kani	Kani backend — 419 proof harnesses
amenable_creusot	Creusot backend — 93 harnesses
amenable_verus	Verus backend — 332 verified proof functions

Verifiers

• Kani (amenable_kani) — bounded model checking over real Rust code via CBMC.
• Creusot (amenable_creusot) — real Pearlite requires/ensures contracts, discharged by SMT.
• Verus (amenable_verus) — native Rust contracts checked by Verus's own SMT-backed toolchain; the only one of the three that runs natively on Windows.

Each backend has real limits on what it can check directly (state-space size, platform gating, missing spec/contract surface for a given std call), and each documents its own strategy for working around them — usually a small, Amenable-owned accommodation model standing in for the real type, with the proof's evidence still hand-linked back to the real type's registration. See each crate's own README (linked in the table above) for the specifics, including how the std::os::windows cluster is handled by all three despite none of Kani/Creusot/creusot-rustc running on Windows.

Status

The core constitutional trait family is implemented with zero runtime dependencies, and all three verifier backends are wired in and actively exercised. The per-backend proof counts in the table above aren't three disjoint slices of std — most tracked types carry proofs from all three backends at once, which is exactly what the aggregate figure below measures directly.

Per the project's own coverage audit (elicit_doc), 421 of 440 accountable stable std/core types (95.7%) have complete evidence plus every applicable verifier's witness. The remaining 19 are either confirmed false-negatives in the audit tool's own type-alias resolution (no real gap) or the std::os::windows cluster's Verus proofs, which are only checkable on the windows-latest CI job mentioned above.

Not yet built: structural proof-quality heuristics on Witness itself (automatic detection of vacuous or corner-cut proofs — amenable.md describes the target design), and the audit-inversion registry (a reverse index from a cited Standard root to every dependent that relies on it, for direct review). Reviewer-driven proof assessment (amenable assess, above) is a separate, already-implemented path that depends on neither — see docs/AMENABLE_PLAN.md for the full phased plan.

License

Licensed under either of:

• Apache License, Version 2.0 (LICENSE-APACHE)
• MIT license (LICENSE-MIT)

at your option.