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.
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 blockchain. Now maintained by o1Labs.
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
Why "Tactic"?
April 24, 2026
The origin of the word tactic in proof assistants, from Robin Milner's LCF to Lean 4.
p-adic Numbers: A Different Idea of Closeness
April 10, 2026
An introduction to p-adic numbers for developers and engineers. We build the p-adic integers from scratch, work through concrete examples, trace the history from Hensel to Scholze, and see how Hensel lifting turns mod-p solutions into exact p-adic roots.
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.
Where to find us soon?
Zcash Dev Summit
May 2026
Rome, Italy.
ZKProof 8
2026
Rome, Italy.
Eurocrypt 2026
2026
Rome, Italy.
zkSummit 14
2026
Rome, Italy.
Past events
EthCC
March 2026
Cannes, France.
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. 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.