Adam Benenson

Founder/CEO at Forethink Labs. Formal methods, agent orchestration, Lean 4, Rust.

Writing

January 2026 · Medium
What changes when AI works inside a formal type system and hallucination is structurally rejected on contact.
January 2026 · Medium
Why Rust's strictness makes it the optimal substrate for agentic coding. The compiler as an unambiguous oracle.
2024 · Medium
On the attention tax of context reconstruction and the case for anticipatory AI tooling.

Working Papers

The Constitution Needs a Compiler
In preparation · 2026
Alignment research has effective systems and no formal account of legitimacy. H. Peyton Young's equity axioms — consistency, solidarity, monotonicity — provide the missing formal backend. Constitutional AI is the right instinct with the wrong substrate.
Stigmergic Governance: A Common Formal Object
In preparation · 2026
Four systems — formal field theory, agent orchestration, self-modeling, and prediction markets — are related by kernel isomorphisms that preserve promotion logic. A transfer theorem: results in one domain hold across all four.

Forethink Labs

A research laboratory building systems that accumulate structured intelligence, govern their own evolution, and compound capability over time — across anticipatory AI tooling, autonomous agent architectures, cognitive modeling, and systematic market intelligence.

Rust · WASM · TypeScript · Svelte
Ambient AI layer for the browser that resurfaces relevant information before you know you need it. The problem it addresses is structural: knowledge workers lose hours daily not to hard problems but to context reconstruction — finding the thing you already found, rebuilding the thread you already held. Most AI tools respond to prompts; Forethink anticipates context, proactively surfacing connections across your digital history as you work. The architecture is local-first and edge-native: all processing happens on-device, with no data extraction or centralized indexing. Privacy isn't a policy — it's the substrate.
Eudaimon
Rust
A recursively self-building entity — a factory for autonomous agent swarms that continuously rewrites its own dispatch logic, capability map, and authority boundaries based on accumulated evidence. It maintains a queryable self-model: not just a record of what it has done, but a structured representation of why decisions produced the outcomes they did, enabling causal attribution and counterfactual reasoning over its own history. Each autonomy expansion is backed by a promotion certificate: a proof object recording the evidence trail, admissibility checks, and rollback witness that authorized it. Candidates move through a typed validation pipeline before earning authority; clawback on degradation is mandatory and automatic. The governance layer isn't a constraint on growth — it is the growth mechanism. A system that can only expand by proving it should.
Adamumbra
Python · Rust · JavaScript
A digital twin — a persistent AI counterparty built to reconstruct and extend one person's causal reasoning, belief structure, and intellectual trajectory. Ingests from 6,600+ conversations, extracts and consolidates structured claims across ten psychological dimensions, maintains a knowledge graph and 11,000-entry profile database. Runs continuous background cycles to improve its own models and scores fidelity against real behavioral traces. The hard question: can a system reconstruct not just what someone said, but how they would reason through a problem they've never encountered — replaying their intellectual process on novel inputs?
Snowball
Rust · live
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. The system autonomously ratchets size as edge compounds — no operator in the loop.

Formal Methods

Stigmergic Field Theory
Lean 4
Formal investigation into how information organizes itself into structure. Starting from a single constraint (absolute indifference is unrepresentable), derives a three-component tensor decomposition (ICU), a variational principle, and a discharge architecture. Built on Mathlib; key results proven sorry-free.
cencov-petz
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. Proved via splitting invariance at rational points + density argument.
compact-spectral
Lean 4 · Mathlib candidate · sorry-free
The spectral theorem for compact self-adjoint operators on Hilbert spaces: a Hilbert basis of eigenvectors exists.
rellich-kondrachov
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.

Background

Novus Partners
Managing Director, Head of Product · 2013–2020
Led the product, engineering, data, and design departments at an enterprise analytics company serving 140+ institutional investors managing $3T+ in assets — hedge funds, sovereign wealth funds, pensions, and family offices. Full org ownership from strategy through execution; member of the executive team.
Diamondback Capital
Quantitative Analyst → Portfolio Manager · 2008–2012
Analyst on a $2B+ systematic equity book (Sharpe above 2) through the 2008–2009 financial crisis; promoted to PM managing own $200M+ portfolio concurrently, from factor research through live risk management.
Board Governor · 2022–present