Invariant – AI LLM Automated Program VerifierJan 2026
Python, Lean 4, C, Gemini API
- Built a GCP pipeline (Docker, Gemini) to generate C and equivalent Lean, verified via Harmonic's Aristotle
- Implemented automated differential testing to verify the Lean code against the C implementation
- Created a feedback loop where Gemini fixes its own errors from compiler warnings and test failures
CalibrationBoard – Prediction Market Data Modeling PipelineFeb 2026
Python, REST APIs, Requests
- Queried the Manifold Markets API with 6,200+ requests across 24,000+ markets, 139,000+ bets, and 5,800+ users
- Scored users with a Kelly criterion calibration metric, ranking forecasters by the lower bound of their 95% CI
- Identified the top 30 forecasters out of 5,851 unique bettors across 341 resolved markets
MeshToSDF – Neural Signed Distance FunctionsMar 2025
Python, NumPy
- Engineered an MLP-based signed distance field that models 3D surfaces from input coordinates
- Added Fourier-feature encodings to sharpen feature representation and reduce low-frequency bias
- Trained on 400,000 sample points, reducing MSE loss 200x from 444 to 2.1 over 12 epochs