Projects

Digital Twin
Python · Rust · JavaScript
A personal digital twin built to reconstruct and extend causal reasoning, belief structure, and intellectual trajectory. Maintains a 24,000-episode store, 12,000-entry profile database, and a queryable knowledge graph. Context engineering formalized as a DT-MDP with a contrastive IRL retrieval policy. Drives daily development across the lab's other systems — including the legitimacy research program below.
Rust · Lean 4 · sorry-free
An Arrow-lineage impossibility theorem for AI governance and a machine-checked semantic legitimacy kernel. A research program in active development.

Forethink Labs

Rust · WASM · TypeScript · Svelte
Ambient AI layer for the browser that resurfaces relevant information before you search. On-device processing, zero data extraction, memory-safe via Rust+WASM sandbox. Full system architected from scratch (~186K LOC).
Workgraph
Rust · Python · TypeScript
A permissioned research-intelligence platform for professional services firms — domain ontologies spanning legal matters and investment research (firms, strategies, factors, themes). Email/Drive change-data-capture into a temporal-hypergraph knowledge graph with tri-temporal indexing; specialized agentic workflows for retrieval, drafting, compliance, and escalation; scoped ACLs with information-barrier enforcement and a full audit plane.
Eudaimon
Rust
A recursively self-building factory for autonomous agent swarms. Every autonomy expansion is backed by a promotion certificate: evidence trail, admissibility check, rollback witness. The governance layer is the growth mechanism — a system that can only expand by proving it should.
Snowball
Rust
A recursively self-learning alpha compounding engine for prediction markets. Hypotheses enter as replay-scored candidates, survive shadow and paper validation, earn size through bounded live review, and get clawed back when evidence degrades. Every fill updates a market factor graph; the graph reshapes candidate selection; better candidates generate more evidence.

Formal Methods

Stigmergic Field Theory
Lean 4
A formal theory of the relationship between information and energy, and how organized structure emerges from their interaction. Derives a variational principle and a three-component tensor decomposition (Integration, Complexity, Uncertainty) from a single information-geometric constraint. Key theorems sorry-free.
Lean 4 · Mathlib · sorry-free
A Lean 4 formalization of Shannon capacity-achieving prior uniqueness for Markov kernels. Three layered theorems: a finite-alphabet result, a compact-Polish discharged result, and a general measure-theoretic packaging result.
Lean 4 · Mathlib candidate · sorry-free
The finite Čencov–Petz uniqueness theorem: any continuous monotone metric family on the probability simplex is a scalar multiple of the Fisher information metric.
Lean 4 · Mathlib candidate · sorry-free
The spectral theorem for compact self-adjoint operators on Hilbert spaces: a Hilbert basis of eigenvectors exists.
Lean 4 · Mathlib candidate · sorry-free
Rellich–Kondrachov compact embedding: H¹ → L² is compact on compact Riemannian manifolds. Euclidean heart via Fréchet–Kolmogorov; manifold glue via finite chart decomposition.