Projects

Pathwise

High-performance SDE simulation toolkit. Rust core with Python bindings via PyO3. Supports Brownian motion, GBM, Ornstein-Uhlenbeck, and custom processes with rayon-parallelised Monte Carlo.

gpufft

Cross-vendor GPU FFT for Rust, backed by VkFFT on Vulkan and cuFFT on CUDA. A single trait surface runs identically on NVIDIA, AMD, and Intel; buffers and plans are typed at the backend-and-scalar level, so mixing a Vulkan buffer with a CUDA plan, or an f32 plan with a Complex64 buffer, is a compile error. plan_c2c, plan_r2c, and plan_c2r at f32 and f64 over 1D, 2D, and 3D. Ships a dual-backend manylinux Python wheel cross-validated against numpy. Sibling to ferrum-gpu, sharing its FFT API.

Cartan

Riemannian geometry on smooth manifolds. Connection forms, parallel transport, holonomy groups, and geodesic flows. Documentation at cartan.sotofranco.dev.

Volterra

Covariant active nematics solver built on Cartan. Dimensionally agnostic: any type implementing cartan_core::Manifold serves as the simulation domain. Beris-Edwards equations on arbitrary Riemannian geometries via discrete exterior calculus.

von Karman

Multi-precision pseudospectral Navier-Stokes solver. ETD-RK4 time integration with Kassam-Trefethen contour integral, dealiased 3/2 cross product, adaptive CFL. Five initial conditions, energy spectrum diagnostics, HDF5 snapshots, Parquet time series.

Elworthy

JIT compiler that specialises Bismut-Elworthy-Li formulas into SIMD kernels for unbiased Monte Carlo Greeks on non-stationary SDEs. Symbolic AST, Cranelift lowering (scalar and 2-lane F64X2), multi-dimensional Heston driver, pathwise and likelihood-ratio Malliavin parameter Greeks (machine-checked with SymPy). European call price and BEL delta cross-validated against Black-Scholes closed form and the independent blackscholes crate; both agree within four Monte Carlo standard errors. About 22x over a tree-walking interpreter on GBM paths.

Kloeden

Hand-written SIMD C++ vs Rust (LLVM + Cranelift) benchmark companion to pathwise and elworthy. Same Brownian-increment fixture across four impls; single-thread pinned-core throughput on scalar Euler / Milstein / Taylor 1.5 on GBM, plus a digital-delta correctness table showing naive pathwise silently returns 0 in both languages while the Bismut-Elworthy-Li constant-flow weight matches analytic within 4 Monte Carlo standard errors (bitwise-identical between hand-rolled C++, hand-rolled Rust, and elworthy_rt::from_paths). Named after Peter Kloeden.

Mermin

$k$-atic alignment analysis of fluorescence microscopy. Minkowski tensor shape descriptors, multiscale structure tensor fields, topological defect detection via cartan-geo $\mathrm{SO}(3)$ holonomy, persistent homology, spatial statistics, and Landau-de Gennes parameter fitting. Outputs calibrated parameters for forward simulation in volterra. 7 crates on crates.io, Python bindings on PyPI.

Meridian

Lean 4 metaprogramming toolkit for mathematical formalisation. Sorry extraction, dependency-graph and theorem analysis, IDA* proof search, goal decomposition, type-class instance debugging, and project-level Mathlib coverage reports. Domain tactics for PDE (distributional derivatives, Sobolev exponent arithmetic, Biot-Savart automation, curvature bounds) and geometric measure theory (rectifiable sets, varifolds, first variation, stationary varifolds). Runs locally: no network calls, no data leaves the machine.

tactic-ranker

Learned premise retriever for Lean 4 and Mathlib4. Two-stage retrieve-and-rerank: hybrid dense plus DiscrTree retrieval, then a distilled cross-encoder. A code-pretrained ModernBERT encoder in place of ByT5, a masked contrastive loss that correctly handles premises shared across proofs, and hard-negative mining across epochs; the sparse channel is Mathlib’s own first-order pattern index, exported from Meridian. Serves live into Meridian over a FastAPI inference server. Benchmarked R@k against ReProver.

Meridian for VS Code

VS Code extension surfacing a live dependency graph, sorry inventory, and Mathlib coverage view for any Lean 4 project. A side panel renders each file’s 2-hop dependency graph colour-coded by proof status, with imports and Mathlib refs resolved through a full-project index; edges are tagged signature versus body so refactor cost is visible at a glance. Runs entirely on your machine: no hosted API, no telemetry.

Polybius

Live Polymarket prediction market engine. BTC/ETH WebSocket price feed drives a 5-minute directional and regime model; orders execute on the Polymarket CLOB via a custom Rust signing layer.

Malliavin

Options volatility surface engine. Multi-agent regime detection, coarse-grained signal emission, vol surface manifold. Deployment target: Deribit and IBKR.

Bismut

Volatility surface manifold toolkit. Malliavin calculus-based Greeks, SDE vol models, and backtest infrastructure for equity derivatives.

inferCNAsc

Copy number variation and ascertainment bias inference for single-cell genomics. Rust compute core with Python bindings via PyO3/maturin. Published on PyPI.

cuda-oxide #117

Merged upstream PR to NVlabs/cuda-oxide. feat(codegen): fma contraction and an opt -O3 pass to match nvcc defaults. Merged 2026-06-18T05:37:45Z.

cuda-oxide #256

Merged upstream PR to NVlabs/cuda-oxide. feat(cargo-oxide): add emit-ltoir to build a crate's LTOIR in one step. Merged 2026-06-20T12:56:37Z.

cuda-oxide #257

Merged upstream PR to NVlabs/cuda-oxide. fix(cargo-oxide): rebuild cached backend when its source advances. Merged 2026-06-20T12:57:09Z.

Mathlib4

Upstream contributions to leanprover-community/mathlib4 — the Lean 4 community mathematics library. PR #40824 (feat(Analysis/FunctionalSpaces): the one-dimensional Poincaré inequality) submitted 2026-06-19, under review. PR #38022 (feat(Topology/Algebra/Support): compact multiplicative support under product operations) merged by Bors.

Gas Leak Rate Calculator

Subsurface safety valve gas leak rate calculator per API RP 14B 5th edition. Dranchuk-Abou-Kassem equation of state. Free, unlimited calculations.