Computer Science graduate working on Lean 4, formal verification, SMT/Z3, and machine-checked mathematics, with a deep background in zero-knowledge cryptography and Rust.

I turn mathematical statements written in natural language into precise, compilable Lean 4 proofs, and I care about more than getting a proof to compile: does the formal statement capture the intended meaning, are the assumptions complete, and does the informal argument hide a logical gap? My ZK work (finite fields, polynomial arithmetic, commitments, proof systems) gives me the mathematical depth to formalize the material I'm most interested in.

Machine-checked Lean 4 proofs and formalizations of mathematical statements, built with Mathlib.

• Formal verification and specification work using Lean 4 and SMT/Z3

Lean 4 Mathlib Theorem Proving SMT Z3 Formal Verification

Educational STARK proving system built from scratch in Rust: finite-field arithmetic, FFT/IFFT, low-degree extension, AIR constraints, composition polynomials, Merkle commitments, Fiat-Shamir transcripts, and FRI folding.

Rust STARKs FRI AIR FFT Finite Fields

KZG implemented from scratch in Rust: SRS and trusted setup, commitments, quotient polynomials, evaluation proofs, and pairing-based verification over BLS12-381.

Rust KZG BLS12-381 Bilinear Pairings

Studied Airbender, a Rust-based RISC-V zkVM prover, tracing how proof-system theory becomes production code. Also investigated Ethereum execution behavior using execution-spec fixtures and differential testing.

Rust zkVM RISC-V Ethereum Execution

Open-source, end-to-end learning roadmap for ZK: math foundations → cryptographic primitives → Groth16, PLONK, STARKs, FRI, Halo, folding → zkVMs and prover engineering. I completed it myself before publishing it for others.

Zero-Knowledge Cryptography Technical Writing Open Source

• evmdecode: Rust EVM analysis toolkit with ABI calldata decoding, transaction simulation, an 844-instruction bytecode parser, and detection of Uniswap V2/V3 swaps, sandwich attacks, and arbitrage. Rust alloy-rs tokio MEV
• SPL Token Staking Program: Solana staking program in Rust and Anchor with PDA-based access control, reward calculation, lock-ups, early-withdrawal penalties, and CPIs. Rust Solana Anchor

Formal Methods: Lean 4 · Mathlib · Theorem Proving · Formal Logic · Formal Verification · SMT · Z3 · Automated Reasoning

Math & Cryptography: Finite Fields · Polynomial Arithmetic · Algebra · FFT/IFFT · Elliptic Curves · Bilinear Pairings · R1CS · QAP · Fiat-Shamir

Zero-Knowledge: Groth16 · PLONK · STARKs · FRI · AIR · KZG · Halo2 · Nova / Folding Schemes · Sumcheck · Lookup Arguments

Engineering: Rust · Solidity · Cairo · Circom · EVM · zkVMs · Git · Foundry · Cargo

• Smart India Hackathon Winner
• TryHackMe: Top 1% globally
• 6 months of professional software engineering experience
• Independent research in ZK systems, formal verification, and protocol security

Primary: Lean 4 Mathematical Formalization · Formal Verification · Theorem Proving · AI + Formal Methods (remote research, contract, or freelance)

Also open to: Junior ZK Engineer · Prover Engineer · Cryptography Engineer · Protocol Engineer · Security Researcher