# Computer Scientists

**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