Welcome to my website on formal verification and cryptography.
What I’m Working On
Cryptographic systems rely on the correctness of their implementations. This website documents my work applying formal methods to strengthen that foundation.
Current Focus:
- RustCrypto: Formally verifying the sha2 and k256 implementations using HAX and F*
- secp256k1: Working on correctness and safety proofs for elliptic curve operations and multi-scalar multiplication in libsecp256k1. Researching which framework and proof assistants work best.
Why Formal Methods?
While code review, testing and fuzzing catch many bugs, formal verification goes further: Proving the absence of entire classes of errors. For critical cryptographic code, this level of assurance matters.
Design flaws in cryptographic protocols are rare and usually caught early. Implementation bugs are more common, particularly in systems languages. Formal methods can prove:
- Memory safety (no buffer overflows, use-after-free, etc.)
- Functional correctness against specifications
- Panic/termination freedom for all possible inputs
The Road Ahead
I’ll be sharing progress updates, technical challenges, and insights from working with different proof assistants and verification tools. The goal is not just to verify individual components, but to develop reproducible methods that can benefit the broader cryptography ecosystem.
Stay tuned for updates on verified cryptographic implementations, lessons learned from proof engineering, and contributions to high-assurance software.
Contact: remix7531@mailbox.org