-
-
Notifications
You must be signed in to change notification settings - Fork 0
Computer Scientists
Your Name edited this page Jan 26, 2026
·
1 revision
proven uses Idris 2 dependent types and totality checking to encode and prove safety properties.
Highlights:
- Proof‑carrying functions in Idris
- RefC backend emits C, linked via Zig ABI
- No trusted logic outside Idris core
Research directions:
- Mechanized verification of cross‑language ABI properties
- Proof‑aware extraction to Zig
- Automated proof checking in CI via echidnabot