Crate ruvector_verified 

Formal verification layer for RuVector using lean-agentic dependent types.

This crate provides proof-carrying vector operations, verified pipeline composition, and formal attestation for RuVector’s safety-critical paths.

Feature Flags

• hnsw-proofs: Enable verified HNSW insert/query operations
• rvf-proofs: Enable RVF witness chain integration
• coherence-proofs: Enable coherence verification
• serde: Enable serialization of proof attestations
• fast-arena: SolverArena-style bump allocator
• simd-hash: AVX2/NEON accelerated hash-consing
• gated-proofs: Coherence-gated proof depth routing
• ultra: All optimizations (fast-arena + simd-hash + gated-proofs)
• all-proofs: All proof integrations (hnsw + rvf + coherence)

Re-exports

pub use error::VerificationError;

pub use error::Result;

pub use vector_types::mk_vector_type;

pub use vector_types::mk_nat_literal;

pub use vector_types::prove_dim_eq;

pub use proof_store::ProofAttestation;

pub use pipeline::VerifiedStage;

pub use invariants::BuiltinDecl;

Modules

cache

Conversion result cache with access-pattern prediction.

error

Verification error types.

invariants

Pre-built invariant library.

pipeline

Verified pipeline composition.

pools

Thread-local resource pools for proof-checking.

proof_store

Ed25519-signed proof attestation.

vector_types

Dependent types for vector operations.

Structs

ProofEnvironment

The proof environment bundles verification state.

ProofStats

Verification statistics.

VerifiedOp

A vector operation with a machine-checked type proof.