About

I’m Keagan McClelland. I work at the intersection of formal verification and Bitcoin protocol engineering.

Eight years on Bitcoin and Lightning protocol development (Lightning Labs, Alpen Labs, Judica) built the domain side. Formal methods — currently Lean 4, with prior Coq exposure and a long Haskell background — built the tooling side. The bet I’m making is that the combination produces infrastructure neither produces alone: Bitcoin consensus changes argued against shared formal models rather than competing intuitions, and verified protocol implementations that live up to their specifications.

This site has two tracks:

• Essays — philosophy, worldview, and the inner life. Less about what I’m building and more about how I think. There Are No Rules, Only Consequences is a representative piece.
• Research — formal verification, Bitcoin protocol engineering, AI-authored verified software. Thesis posts and positioning pieces; code lives on GitHub and protocol-level work on delving-bitcoin and the Lean Zulip.

Each track has its own Atom / RSS (research / rss) feed, plus a combined feed if you want everything. The audiences barely overlap; the feeds let you self-select.