I'm mostly a hands-on person, but that doesn't stop me from seeking out the offerings of formal methods. As part of my PhD, I work in an area that bridges low-level systems programming and formal verification backed by type theory.
My algorithm improving the precision of tnum multiplication is now part of the upstream Linux kernel eBPF verifier. This repo contains the benchmark code and some explanation. I will update this page once the paper is published.