Code that cannot crash.
- The Problem
- The Solution
- What "Mathematically Proven" Means
- Modules
- SafeMath — Arithmetic That Can’t Overflow
- SafeString — Text That Can’t Corrupt
- SafeJson — Parsing That Can’t Fail Unexpectedly
- SafeUrl — URLs That Can’t Be Exploited
- SafeEmail — Validation That Actually Works
- SafePath — Filesystem Access That Can’t Escape
- SafeCrypto — Cryptography You Can’t Mess Up
- SafePassword — Authentication Done Right
- Installation
- How It Works (For the Curious)
- FAQ
- Roadmap
- Contributing
- Related Projects
- License
- Security
# Your code at 3am
result = 10 / user_input # ZeroDivisionError
data = json.loads(response)["key"] # KeyError
url = urllib.parse.urlparse(user_url) # Malformed URL? Who knows
password = hashlib.md5(pwd).hexdigest() # You just got hackedEvery one of these will crash your app or create a security hole.
from proven import SafeMath, SafeJson, SafeUrl, SafePassword
# Cannot crash. Ever. Mathematically proven.
result = SafeMath.div(10, user_input) # Returns None if zero, not an exception
data = SafeJson.get(response, "key") # Returns None if missing, typed if present
url = SafeUrl.parse(user_url) # Returns structured error or valid URL
hashed = SafePassword.hash(pwd) # Argon2id, timing-safe, correct parametersThis isn’t marketing fluff. Here’s what makes proven different from regular libraries.
Every function in proven is written in Idris 2, a language with dependent types. The compiler literally proves your code is correct before it runs.
In most languages, types are separate from values:
def get_first(items: list) -> int:
return items[0] # Crashes if empty!The type system has no idea if the list is empty. It just trusts you.
In Idris 2, types can depend on values:
-- This type signature REQUIRES a non-empty list
getFirst : (items : List Int) -> {auto prf : NonEmpty items} -> IntThe {auto prf : NonEmpty items} part means: "The caller must provide proof that items is non-empty." If you try to call this with an empty list, the code won’t compile.
This is the core insight: instead of runtime crashes, we get compile-time errors.
| Regular Code | Proven Code |
|---|---|
"I think this won’t crash" |
"The compiler proved this cannot crash" |
"I tested it and it worked" |
"Every possible input was checked at compile time" |
"It passed code review" |
"A theorem prover verified it" |
The proofs are available in src/Proven/ and we encourage you to explore them! Understanding dependent types is a valuable skill. Here are some resources:
-
Idris 2 Tutorial — Official introduction to dependent types
-
Type-Driven Development with Idris — Edwin Brady’s talk
-
Our proof documentation — Explains each proof in this library
That said, you can absolutely use the library without understanding the proofs—the whole point of formal verification is that the compiler has already checked correctness for you.
| Function | What It Does | What It Prevents |
|---|---|---|
|
Safe division, returns |
|
|
Addition with overflow detection |
Silent integer overflow |
|
Multiplication with overflow detection |
Integer overflow exploits |
|
Safe modulo |
Division by zero |
|
Absolute value (handles MIN_INT) |
Overflow on |
from proven import SafeMath
SafeMath.div(10, 2) # 5
SafeMath.div(10, 0) # None (not an exception!)
SafeMath.add_checked(2**63 - 1, 1) # None (overflow detected)
SafeMath.add_checked(5, 3) # 8| Function | What It Does | What It Prevents |
|---|---|---|
|
Safe UTF-8 decoding |
|
|
SQL injection prevention |
SQL injection attacks |
|
XSS prevention |
Cross-site scripting |
|
Safe truncation (respects graphemes) |
Slicing mid-emoji |
from proven import SafeString
SafeString.decode_utf8(b"\xff\xfe") # None (invalid UTF-8)
SafeString.decode_utf8(b"hello") # "hello"
SafeString.escape_sql("'; DROP TABLE users;--")
# "'' ; DROP TABLE users;--" (neutralized)| Function | What It Does | What It Prevents |
|---|---|---|
|
Safe JSON parsing |
|
|
Safe key access |
|
|
Safe nested access |
Chained |
|
Typed extraction |
Type confusion |
from proven import SafeJson
data = SafeJson.parse('{"name": "Alice", "age": 30}')
SafeJson.get(data, "name") # "Alice"
SafeJson.get(data, "missing") # None
SafeJson.get_int(data, "age") # 30
SafeJson.get_int(data, "name") # None (wrong type)
SafeJson.parse("not json") # Error object with details, not exception| Function | What It Does | What It Prevents |
|---|---|---|
|
RFC 3986 compliant parsing |
Malformed URL crashes |
|
Open redirect prevention |
Open redirect attacks |
|
URL normalisation |
URL bypass attacks |
|
Path without traversal |
|
from proven import SafeUrl
url = SafeUrl.parse("https://example.com/path?query=1#hash")
url.scheme # "https"
url.host # "example.com"
url.path # "/path"
SafeUrl.parse("not a url") # Error object, not exception
SafeUrl.is_safe_redirect(
"https://evil.com",
allowed=["example.com"]
) # False| Function | What It Does | What It Prevents |
|---|---|---|
|
RFC 5321 compliant check |
Bad regex accepting invalid emails |
|
Extract local/domain parts |
Injection via email fields |
|
Lowercase, trim, normalise |
Case sensitivity bugs |
from proven import SafeEmail
SafeEmail.is_valid("user@example.com") # True
SafeEmail.is_valid("not an email") # False
SafeEmail.is_valid("user@localhost") # True (valid per RFC)
email = SafeEmail.parse("User@Example.COM")
email.local # "User"
email.domain # "example.com" (normalised)| Function | What It Does | What It Prevents |
|---|---|---|
|
Safe path joining |
Path traversal attacks |
|
Check containment |
Directory escape |
|
Remove dangerous chars |
Null byte injection, special chars |
from proven import SafePath
SafePath.join_safe("/var/uploads", "file.txt")
# "/var/uploads/file.txt"
SafePath.join_safe("/var/uploads", "../../../etc/passwd")
# Error: path traversal detected
SafePath.sanitize("file\x00.txt") # "file.txt" (null byte removed)| Function | What It Does | What It Prevents |
|---|---|---|
|
SHA-3 hashing |
Using broken algorithms |
|
BLAKE3 hashing |
Slow hashing |
|
Cryptographic randomness |
Using |
|
Timing-safe comparison |
Timing attacks |
from proven import SafeCrypto
# Cryptographic randomness (not random.random()!)
token = SafeCrypto.random_bytes(32)
# Secure hashing
digest = SafeCrypto.hash_sha3(b"data")
digest = SafeCrypto.hash_blake3(b"data") # Faster
# Timing-safe comparison (prevents timing attacks)
SafeCrypto.constant_time_eq(user_token, stored_token)| Function | What It Does | What It Prevents |
|---|---|---|
|
Argon2id hashing |
MD5, SHA1, bcrypt weaknesses |
|
Timing-safe verification |
Timing attacks |
|
Strength checking |
Weak passwords |
from proven import SafePassword
# Hash with Argon2id (current best practice)
hashed = SafePassword.hash("user_password")
# Verify (timing-safe)
if SafePassword.verify("user_password", hashed):
print("Login successful")
# Strength check
SafePassword.is_strong("password123") # False
SafePassword.is_strong("c0rr3ct-h0rs3-b4tt3ry-st4pl3") # TrueDeno (recommended):
import { SafeMath, SafeJson } from "jsr:@proven/core";Node.js:
npx jsr add @proven/coreUsing pipx (recommended for isolated environments):
pipx install provenUsing pip:
pip install proven|
Tip
|
pipx installs packages in isolated virtual environments, preventing dependency conflicts and improving security. Install it with pip install pipx if you don’t have it.
|
┌─────────────────────────────────────────────────────────────────┐
│ Your Python/Rust/JS App │
└──────────────────────────┬──────────────────────────────────────┘
│ import proven
▼
┌─────────────────────────────────────────────────────────────────┐
│ Language Bindings (auto-generated) │
│ Python: ctypes | Rust: bindgen | JS: WebAssembly │
└──────────────────────────┬──────────────────────────────────────┘
│ C ABI
▼
┌─────────────────────────────────────────────────────────────────┐
│ Zig FFI Bridge Layer │
│ Cross-platform • Memory safe • Stable ABI guaranteed │
│ (see: github.com/hyperpolymath/idris2-zig-ffi) │
└──────────────────────────┬──────────────────────────────────────┘
│
▼
┌─────────────────────────────────────────────────────────────────┐
│ Idris 2 Verified Core │
│ │
│ • Dependent types: compiler PROVES code is correct │
│ • Total functions: every input produces valid output │
│ • No runtime exceptions: impossible by construction │
│ │
│ Used by: aerospace, automotive, financial, blockchain │
│ Inspiration: HACL* (Firefox, Linux kernel, WireGuard) │
└─────────────────────────────────────────────────────────────────┘Q: Is this slow?
No. Idris 2 compiles to C, then Zig optimises it. Benchmarks show performance within 5-15% of hand-written C for most operations. Crypto functions are often faster because they use constant-time implementations that avoid branch misprediction.
Q: Do I need to learn Idris 2?
Not required, but encouraged! The library bindings work like any standard library in your language. However, if you’re interested in formal verification, understanding the Idris 2 source code will help you appreciate why the guarantees are so strong. See the "Want to Learn More?" section above for resources.
Q: What if I find a bug?
If you find a bug in proven, you’ve likely found a bug in either: 1. The language bindings (our bug, please report) 2. The Idris 2 compiler (extremely rare) 3. Your understanding of the function (check the docs)
The core logic is mathematically proven. But the bindings are written by humans.
Q: Why not just use existing libraries?
| Library | Problem |
|---|---|
|
Throws exceptions on invalid input |
|
Lets you use MD5, SHA1, and other broken algorithms |
|
Complex API, easy to misuse, path traversal possible |
|
Truncates passwords at 72 bytes silently |
|
Not cryptographically secure (people use it for tokens anyway) |
Q: Is this production ready?
Not yet. We’re targeting 1.0 in Q4 2025. Star the repo to follow progress.
-
❏ SafeString, SafeJson, SafeUrl, SafeEmail, SafePath
-
❏ Rust, JavaScript, Deno bindings
-
❏ Test suite
We welcome contributions! See CONTRIBUTING.adoc.
Especially needed: - Language binding maintainers (Go, Java, C#, Swift) - Security reviewers - Documentation writers - Test case contributors
| Project | What It Is |
|---|---|
The FFI bridge that makes this library callable |
|
Idris 2 static site generator (first consumer) |
|
Verified crypto in Firefox, WireGuard, Linux (our inspiration) |
Palimpsest-MPL-1.0. See LICENSE.
Commercial licensing available for proprietary use.