Systems Engineering · Low-Latency · Post-Quantum · Blockchain · Quantum
Lock-free/wait-free data structures, formally verified
379M ops/secPost-quantum blockchain with native SQL, on-chain DEX
996 testsGPU-accelerated HFT backtester with Aria language for fast strategy development
49K events/secReal-time market data terminal, PQ encrypted
17 feed adaptersFPGA meta-compiler: from DSL to silicon with formal proofs. 10 backends (Verilog, VHDL, CUDA, Metal, Lean 4)
10 backendsSecure memory: guard pages, mlock, encrypted enclaves, post-quantum KEM
Experiments with the formalization of numerical algorithms
Iris-style concurrent separation logic, mechanized in Lean 4: fancy updates, world satisfaction, invariants — proved sorry-free.
A harness for building tools with local models: a ReAct agent loop with world-model lookahead, and distillation of large agent models into small local students (1B / 3B / 8B). Built to drive leanlift and the security toolkit.
RustComputer-vision toolkit: structure-from-motion from video, OCR, and pluggable feature descriptors.
C++Agents for security. A scanner orchestrator (SAST / DAST / SCA / secrets) with LLM-assisted triage and agent-assisted pen-testing over a SARIF + DuckDB store. Companion to Seal DAO.
GoSimple, composable Rust libraries for building agent tooling fast from a harness: TUI widgets, networking, a capability-scoped shell, secrets, remoting, and a sandbox.
7 libraries →