Notes

Written word.

Not recently updated. Links may have broken since the website was moved.

Series

Formally Verifying Jolt Bytecode Expansions 2026-04-11
Proof Complexity Notes
Money For Nothing Monads For Free 2026-03-25

Posts

Compiling RISCV-SAIL Into Lean4 Cpuu 2026-03-22
Lost in Translation 2026-03-09
Sumchecks Bloody Sumchecks 2026-02-20
Anatomy Of A Jolt Sumcheck 2025-12-01
Small Scalar Binding 2025-10-04
Tracked Types 2025-10-04
Algorithms For Montgomery Multiplication 2025-05-16
Montgomery Multiplication: Theory Vs Practice 2025-05-15