-
-
Notifications
You must be signed in to change notification settings - Fork 0
Home
Your Name edited this page Jan 26, 2026
·
2 revisions
proven is a safety library where security properties are mathematically proven in Idris 2. The only code considered “unbreakable” is Idris itself; the Zig layer is a pure ABI bridge and must contain no safety logic.
Key points:
- Idris2 proofs guarantee correctness (totality + dependent types)
- Zig is ABI only (no logic)
- Language bindings are thin wrappers calling Idris code
- This trades performance for correctness; we optimize by reducing FFI crossings