Projects

Machine-Checked AI Governance

Rust · Lean 4 · sorry-free · v1.0.0 public
The rules that decide what an AI agent may do — which tool runs, what is escalated to a human, which of several competing requests gets the one scarce review slot — are an agent's governance layer, and today they are mostly unverified scripts. Legitimacy asks whether that rule is even coherent, and proves an impossibility: on scarce, peer-relative surfaces no rule can satisfy every reasonable guarantee at once, so a legitimate one must declare what it sacrifices. A Rust audit pipeline extracts governance graphs from real agent-harness source and checks them against the kernel's obligations; the Lean 4 / Mathlib development is sorry-free. Read the six papers on the site or get the signed release from the repository.

Quantitative Systems

Prism
Python · Svelte · CPCV/DSR-gated
A general-purpose portfolio-intelligence engine. Bayesian view translation (entropy pooling over Black-Litterman), instrumented-PCA factor decomposition, RMT-cleaned covariance (Bouchaud RIE, Ledoit-Wolf NLS), sparse-cardinality mean-CVaR optimization, graphical-matching pair selection, and an immutable decision ledger. Every result must survive a deflation-aware validation battery — combinatorially-purged cross-validation, deflated Sharpe, probability of backtest overfitting — before it is allowed to claim anything. In production in a live long/short equity consulting engagement, driving book analytics, hedge construction, and optimization counterfactuals.
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.

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.
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.
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.

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.