JP Aumasson

JP Aumasson

@veorq · Twitter ·

proof of 0 = 1 in Lean, exploiting a hash collision (weak 32-bit hash Expr.hash/mixhash) https://github.com/endrazine/lean-cve-poc