BaDaaS
We use abstract mathematics to build concrete applications.
Making the Internet better.
A group of mathematicians turned engineers, based in Belgium, Europe, with broad interests in applied mathematics.
We specialise in applied cryptography, formal verification, and AI tooling. From zero-knowledge proof systems to post-quantum cryptography, from machine-checked proofs in Lean 4 to open-source infrastructure, we work across the full stack of mathematical engineering.
What we do
Research
Research
Applied mathematics, cryptography, zero-knowledge proofs, post-quantum cryptography, and formal verification. We contribute to open knowledge and advance the foundations that everything else builds on.
Engineering
Engineering
We build and maintain software, from low-level cryptographic libraries to full infrastructure. Distributed systems, networking layers, proof systems, open source tooling, and production systems.
Projects
Projects
We explore and develop projects that make the Internet safer and knowledge more accessible. LeakIX, Cryptography Academy, and Papyrus all started here.
Security
Security
Attack surface management, cryptographic audits, and vulnerability research. The applied side of our mission to protect the Internet.
Consulting
Consulting
We bridge mathematics and industry across Europe. From cryptographic protocol design to security audits, we help organizations apply formal verification, zero-knowledge proofs, and applied cryptography to solve real engineering problems.
Track Record
2020
Founded
2
Protocols contributed to
5+
Publications and talks
BE
Based in Belgium
Selected engagements
Mina Protocol
Zero-Knowledge Proofs
Core contributor to the Mina Protocol with o1Labs. Contributed to Kimchi (proof system), Pickles (recursive composition), and o1vm (zkVM for MIPS). Drafted Arrabbiata (folding-based proving system). Cryptographic primitives and protocol-level logic in OCaml and Rust.
Tezos
Protocol Development
Protocol-level development and cryptographic research for the Tezos ecosystem with Nomadic Labs. Core infrastructure, ZK rollups, and low-level cryptographic engineering in OCaml.
LeakIX
Co-founded by BaDaaS
Internet-wide attack surface management platform, co-founded and actively developed by BaDaaS. Indexes misconfigurations and vulnerabilities across the Internet with responsible disclosure. 100+ clients.
B2C2
Trading Infrastructure
First engineer at B2C2, now a leading institutional digital asset market maker (London, Standard Chartered partner). Built exchange interfaces, real-time blockchain transaction detection, accounting systems, and risk management pipelines for the trading desk. Maintained multi-chain node infrastructure. 2017 - 2020.
Research
Anemoi
2022
New Design Techniques for Efficient Arithmetization-Oriented Hash Functions: Anemoi Permutations and Jive Compression Mode
C. Bouvier, P. Briaud, P. Chaidos, L. Perrin, R. Salen, V. Velichkov, D. Willems
PlonK
2022
New optimization techniques for PlonK's arithmetization
M. Ambrona, A.-L. Schmitt, R. R. Toledo, D. Willems
RML
Master's Thesis, 2017
To a typed language for modular programming
D. Willems. Directed by F. Pottier (INRIA Paris)
ZK Summit 11
2024
o1VM: Building a Real-World zkVM for MIPS. Bitwise operation encoding, folding schemes, and RAM lookups.
SevenX Research Day
2024
A zkVM for the MIPS architecture and OP fault proofs.
ZKProof 5
Tel Aviv, 2022
Anemoi & Jive: New Arithmetization-Oriented Tools for PlonK. With C. Bouvier.
Open Source
Mina Protocol
2023 - 2026
Core contributor to the Mina Protocol. Contributed to Kimchi (proof system), Pickles (recursive composition), and o1vm (zkVM). Drafted Arrabbiata (folding-based proving). OCaml and Rust.
Octez
2020 - 2023
Core contributor to the Tezos blockchain node. Protocol development, ZK rollup (Epoxy), and low-level cryptographic engineering with Nomadic Labs.
ocaml-bls12-381
2020 - 2023
Efficient OCaml implementation of the BLS12-381 pairing-friendly curve. FFT, multi-scalar exponentiation, hash-to-curve, and signature schemes. Used in the Tezos protocol.
Plompiler
2021 - 2023
Monadic DSL for PlonK circuit development. Includes an optimizer, flamegraphs for constraint profiling, and built-in cryptographic primitives (Anemoi, Poseidon, Rescue, Griffin).
Mina Explorer
2026
Blockchain explorer for Mina Protocol networks. Browse blocks, transactions, and account activity across Mina's zero-knowledge proof chain.
Zcash Web Wallet
Browser-based Zcash wallet with shielded transaction support. Handles zk-SNARK proof generation client-side for private transfers without trusting a server.
Zcash Infra
2025 - 2026
Infrastructure tooling for deploying and managing Zcash full nodes and related services. Automated provisioning, monitoring, and maintenance.
Cryptography Academy
Free educational platform for cryptography and mathematics. Open to everyone.
Papyrus
Distributed pipeline powering Cryptography Academy. Harvests papers from IACR ePrint, converts PDFs to Markdown via GPU, extracts mathematical entities with LLMs, and formalizes them in Lean 4. Open to contributors.
Latest Posts
Who Trained Your AI, and Can You Prove It?
March 14, 2026
The web's implicit contract is breaking. AI crawlers consume content without receipts, and no one can cryptographically prove what trained a model. We explore the legal, technical, and mathematical landscape of AI training accountability.
Hello, World
January 23, 2026
Welcome to the BaDaaS blog. We'll be sharing technical articles on cryptography, security, and software development.
Where to find us soon?
EthCC
March 2026
Cannes, France.
Zcash Dev Summit
May 2026
Rome, Italy.
ZKProof 8
2026
Probably.
Eurocrypt 2026
2026
Probably.
zkSummit 14
2026
Probably.
Team
Danny Willems
Founder
Mathematician turned engineer with broad interests in applied mathematics. Danny founded BaDaaS in Belgium to work on the problems he cares about: cryptography, formal verification, AI tooling, and open-source software.
His work spans zero-knowledge proof systems (SNARKs, folding schemes), symmetric and post-quantum cryptography, machine-checked proofs in Lean 4, and LLM-assisted formalisation pipelines. Before starting BaDaaS, he was the first engineer at B2C2, a leading institutional digital asset market maker now partnered with Standard Chartered. He then spent several years as a core contributor to zero-knowledge proof systems at o1Labs (Mina Protocol) and on protocol-level cryptographic engineering at Nomadic Labs (Tezos).
He studied mathematics with a minor in computer science and physics at UMONS, and completed his master thesis at INRIA under the supervision of Francois Pottier in the Gallium team.