Hibikari: 389 Theorems, 7 Contracts, Zero Knowledge How we formally verified a privacy protocol with 389 Lean 4 theorems, 7 Compact smart contracts, and zero compromises.
Proving Sonoluminescence in Zero Knowledge: How We Built a 1,664-Byte Proof for Real Physics A 3,500-line Rust codebase proves correct execution of a sonoluminescence simulation in zero knowledge. The proof is 1,664 bytes. Verification takes 2.5ms. The hardest part was arithmetic.
Why Fixed-Point Arithmetic is the Hardest Part of ZK Your f64 has 53 bits. Your field has 255. Here's where they collide — and why fixed-point arithmetic is the single hardest problem in ZK circuit design.