Formally verified programming language with security properties proven in Coq. Zero external dependencies. Thousands theorems. 0 admits.
-
Updated
Sep 8, 2026 - Rust
Formally verified programming language with security properties proven in Coq. Zero external dependencies. Thousands theorems. 0 admits.
A provably-bounded, compositional AI architecture. Seven pillars enforcing information-flow security, differential privacy, calibrated uncertainty, and Lyapunov stability — with the security-critical gates machine-checked by SMT over unbounded reals.
Under reconstruction for proof validation of non-interference boundaries
A zero-dependency, partitioned-trust LLM control layer: untrusted data can change what a model says, but provably not what it's allowed to do.
Go PoC for ASM-based behavioral attestation of information-flow non-interference in a concurrent multi-level stack. Companion artifact for our MEMOCODE 2026 paper.
To associate your repository with the non-interference topic, visit your repo's landing page and select "manage topics."