This talk presents a new system for verifiable computing using the Binius proof library. Binius implements a hash-based SNARK built on towers of binary fields, which unlocks huge gains in computational efficiency compared with traditional SNARKs, particularly when using specialized hardware. Programs are written in a simple, statically-typed functional language similar to Standard ML, which compiles directly to a custom virtual machine optimized for cryptographic proofs. By co-designing the VM’s instruction set and compiler with the Binius cryptographic library, we enable practical use cases like compressing Merkle tree proofs, aggregating hash-based signatures, and recursive SNARK proofs.