Type-theoretic verification kernel for formally verified database queries, providing dependent, linear, session, quantitative, effect, and modal type coverage. Idris 2 formal specs, Rust verification kernel, Zig FFI bridge, JSON-RPC protocol. The "LLVM of type safety" for query validation.
rust open-source dependent-types database formal-verification linear-types research-software idris2 typed-dsl temporal-database hyperpolymath affinescript ephapax epistemic-infrastructure epistemic-computing verification-kernel veridical-computing proof-carrying-queries
-
Updated
Sep 27, 2026 - Rust