A u64 is a box that holds 64 bits. Multiply two large u64s and the true product might need 128 bits. The box doesn’t grow — it just wraps. No panic, no warning. Your code runs fine and returns a number that looks reasonable and is wrong.
Cryptography is modular arithmetic on bounded integers. That gap — between “the number” and “the number that fits in the box” — is exactly where the bugs live. Not bad formulas. Correct formulas, on the wrong number.
a = b = 5_000_000_000
m = 2^64 - 59 # largest u64 prime
(a * b) % m = 6553255926290448384
# off by 59
# a*b overflowed the u64
((a as u128 * b as u128) % m as u128) as u64 = 6553255926290448443
# correct
Same formula, same inputs. The only difference is the box the multiply happens in.
That’s the problem coprime is built around. It’s a zero-dependency, no_std number-theory library for u64: gcd, modular exponentiation, CRT, Jacobi and Kronecker symbols, integer roots, deterministic primality, factoring. The whole classical toolkit, but built so a machine checks each primitive rather than asking you to take it on faith.
Two formal tools do the checking. Kani runs bounded model checking on the actual compiled Rust — it bit-blasts u128 at full width, honors real overflow semantics, and cannot be fooled with an assume. It proves 17 harnesses over bounded symbolic slices of the input space. Aeneas extracts the Rust into a functional model and proves 24 primitives against Lean/Mathlib over the full u64 domain, unbounded.
One word is kept strict throughout: “proved” means one of those two tools, at exactly the scope stated. Everything else is “tested.” Testing can show bugs are present. It cannot show they’re absent. The docs say which is which for every function.
The attack index (ATTACKS.md) opens with “Proof of Concept or GTFO” and means it: 23 runnable attacks — DH man-in-the-middle, RSA via Wiener’s small private exponent, DSA nonce reuse, SRP zero-key bypass — each one a runnable test or bracketed as not yet built. Nothing in between.
Stage One is public, secret-free arithmetic. No constant-time guarantees yet, and the docs say so plainly. This is a study in verification, not a library to guard real secrets with.