A field guide to Lean 4's typeclasses, in the spirit of the Haskell Typeclassopedia.

There is a question I keep coming back to, especially now that formal verification is being positioned as a serious engineering tool rather than an academic curiosity: what does a proof actually gu...

Proving the shift-and-add Mersenne modulo trick correct in Lean 4.

A record of the Lean4 tactics I reach for most often, from simp to omega.

Using Lean4 to build formal golden models for RTL verification.

Verifying a floating-point multiplier with Synopsys DPV and case-splitting techniques.

Exploring carbon nanotube computing and its potential impact on GPUs and high-performance computing.

An overview of cache coherency challenges and coherence protocols in multicore systems.

On how layered abstraction in computing connects to category theory.

First post introducing the blog: research, coding projects, and lessons learned.