# Developers

**proven** gives you safety functions you can rely on, across many languages, with correctness proven in **Idris 2**.

What to know:
- All safety logic lives in Idris.
- Zig is a pure ABI bridge.
- Your language binding is a thin wrapper.

Usage model:
1. Call binding function
2. Zig ABI forwards to Idris
3. Idris returns a proven result

If you see non‑Idris logic in a binding, treat it as **unsafe** and report it.