BaDaaS
We use abstract mathematics to build concrete applications.
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.
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.
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
High Assurance Cryptography: A snapshot of the landscape
April 26, 2026
An overview of the high assurance cryptography ecosystem: the companies, research labs, tools, programming languages, products, and cryptographic primitives that make up the world of formally verified and rigorously engineered cryptographic software.
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.
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.