Formally verified programming language with security properties proven in Coq. Zero external dependencies. Thousands theorems. 0 admits.
-
Updated
Aug 13, 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
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.
Add a description, image, and links to the non-interference topic page so that developers can more easily learn about it.
To associate your repository with the non-interference topic, visit your repo's landing page and select "manage topics."