The README makes claims. This file backs them up.
Claim 1: "Mathematically proven safe operations. Code that cannot crash, verified with Idris2 dependent types and totality checking."
How it works: The 104 core safety modules in src/Proven/ are written in Idris2 with %default total, meaning every function is proved to: (1) terminate (no infinite loops), (2) cover all input cases (no pattern match exceptions), and (3) return a value (no throwing runtime exceptions). Dependent types encode preconditions as types (e.g., SafeDiv : (a : Nat) → (b : Nat) → (h : NonZero b) → Nat requires a proof that b is nonzero before dividing). The Idris2 compiler enforces these proofs at compile time. Examples: SafeMath.rs proves arithmetic never overflows (returns Result or bounded nat); SafeString.rs proves buffer bounds are checked before reading. FFI bindings call these verified functions only—no reimplementation in other languages.
Caveat: Verification covers correctness (no crashes, no undefined behavior), not functional correctness (the algorithm might be wrong). Also, Idris2 proved code is only safe if the FFI bridge (ffi/zig/) correctly marshals data. If Zig FFI incorrectly casts types or ignores preconditions, safety claims are violated. Hypatia scans prove this doesn’t happen (0 unsafe patterns in critical FFI code).
Evidence: src/Proven/SafeMath.idr with %default total and dependent type proofs; src/Proven/SafeString.idr with bounds-checked buffer operations. FFI in ffi/zig/src/main.zig calls verified functions only. Test suite: 49 tests passing, 0 believe_me count (eliminated via ADR-008).
How it works: Bindings follow a strict FFI-only pattern (ADR-008 in .machine_readable/6a2/META.a2ml). Language-specific bindings (Rust, Zig, Deno, etc.) in bindings/<lang>/ are thin wrappers that: (1) accept user input in the target language, (2) marshal to C types, (3) call the Zig FFI (ffi/zig/), (4) unmarshal results back. No safety logic lives in bindings—only data conversion. This enables many targets without N reimplementations. A breaking change to SafeMath is fixed once in Idris2, recompiled to Zig, and all bindings immediately use the fixed code.
Caveat: Bindings are scaffolded — most languages are partially implemented. Incomplete bindings may lack support for all SafeMath operations or all 104 modules. Production focus: Rust, Zig, C first; others are aspirational. Pre-submission hypatia scans enforce 0 HIGH/CRITICAL findings before publishing to opam, crates.io, Hex.pm. Python/Cython bindings were deleted 2026-05-27 in line with the estate-wide Python ban (see hyperpolymath/standards language policy).
Evidence: bindings/rust/safe_math.rs calls proven FFI via unsafe { proven_ffi_safe_add(…) }; bindings/zig/src/safe_math.zig wraps the same FFI directly; .machine_readable/6a2/META.a2ml documents ADR-008; hypatia-v2 . --severity critical --severity high confirms 0 findings.
| Technology | Learn More |
|---|---|
Idris2 |
Dependent types, |
Zig |
C ABI bridge, FFI compilation, zero-cost abstractions |
RefC |
Idris2 reference compiler (compiles to C) |
104 Target Languages |
C, Rust, AffineScript, Deno, Gleam, Erlang, Ada, Idris2, Zig, etc. (Python and ReScript bindings were removed per estate language policy — see |
| Path | Purpose |
|---|---|
|
Idris2 core (THE TRUTH): 104 modules, all with |
|
Arithmetic proofs: overflow-safe add/sub/mul/div, bounded nat, checked operations |
|
String buffer bounds, encoding safety, slicing without panics |
|
Floating-point proofs: no NaN, denormal, infinity handling, comparison stability |
|
Memory buffer safety: bounds on read/write, offset validation |
|
Command-line argument parsing without buffer overflows |
|
JSON parsing with size limits, nesting depth checks |
|
URL parsing with RFC compliance, no XXE/SSRF, host validation |
|
Cryptographic operations: key size proofs, algorithm validation |
… |
(99 more modules across security, web, data formats, system I/O, etc.) |
|
C ABI bridge layer |
|
Wraps Idris2 RefC output, exposes C functions for each Safe* module |
|
Builds Idris2 code to .o files, links with Zig, outputs shared library |
|
Language-specific thin wrappers (18 complete, 102 scaffolded) |
|
Rust bindings: safe_*.rs files call proven FFI via unsafe { } |
|
Wraps proven_ffi_safe_add, proven_ffi_safe_mul, etc. |
|
Zig language binding (calls FFI directly; necessarily Zig) |
|
AffineScript binding ( |
|
C header files and static library linking instructions |
|
Language-specific test harnesses (call FFI, verify results) |
|
Architecture diagrams, ADRs, FFI safety guarantees |
|
Architecture decisions: ADR-008 (FFI-only), ADR-009 (120+ targets) |
| Project | Integration | | panic-attacker | Scans bindings with hypatia for unsafe patterns (unwrap, getExn, expect) | proof-of-work | Puzzle arithmetic uses proven SafeMath for overflow safety | vql-ut | VeriSimDB uses proven SafeBuffer for result set marshaling | reposystem | Graph validation uses proven SafeGraph for cycle detection proofs