Blog
Where mathematics meets the real world. We explore how cryptography, formal verification, and applied mathematics solve concrete problems across security, infrastructure, and industry. RSS
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.
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.