open source
A dependently typed programming language and compiler for AI learning systems. Compiles model mathematics, training loops, host code, and GPU instructions into self-contained executables without conventional machine-learning runtimes.
- Trained a 1.38B-parameter language model over 5.84B tokens on two H100 GPUs, averaging 247,865 tokens/sec with an Alpha-generated executable.
- Built native NVIDIA GPU code generation, FP8 kernels, attention, multi-GPU NVLink communication, and direct driver interfaces without CUDA, PyTorch, or NCCL on the training path.
- Developing dependent types, formal verification, and compiler infrastructure for agent-driven discovery of new algorithms and learning systems.
open source
Founded the open standard for representing resumes as JSON. Now an ecosystem of schemas, themes, developer tools, AI job matching, and agent integrations.
- 7,000+ GitHub stars across the ecosystem and tens of thousands of users.
- 52 first-party themes, a public registry, in-browser editor, CLI, and MCP integrations.
- AI job matching with embeddings, hybrid retrieval, and LLM reranking; improved precision at five from 0.2 to 0.8 in evaluation.
- Maintains the schema, CLI, core libraries, jobs package, and Rust serialization tooling.
open source
Co-founded one of the web's largest open-source JavaScript and CSS content delivery networks, now operated with Cloudflare.
- Used by millions of websites and serves billions of requests monthly.
- 10,000+ GitHub stars.
- Helped establish a community-maintained infrastructure project that became a widely used part of the web.
application
An evidence-first knowledge system for AI agents, built in Rust and PostgreSQL. Stores contradictory claims with provenance, bitemporal history, query-time reconciliation, and formal verification.
- 42M+ statements and millions of evidence links, with large-scale LLM extraction and agentic-memory tooling.
- Custom query language, predicate alignment, temporal reasoning, and provenance-aware access control.
- 62 Lean 4 theorems proving core invariants, plus signed and reproducible knowledge releases.
application
An experimental computing platform where language models generate literal executable machine bytes rather than source code, which are validated and executed on a custom virtual computer.
- Designed the ANMA-1 virtual instruction set, validator, interpreter, and WebAssembly execution path.
- Built an interactive browser-based virtual computer with memory, registers, devices, and visual execution tracing.
- Developed checker-assisted agent loops, independent correctness tests, and formal verification experiments.
Bode
Sep 2026application
Developing a general-purpose agent execution harness for persistent sessions across web, CLI, and local development environments.
- Designing durable agent orchestration, resumable sessions, and execution across local devices and remote workers.
- Exploring multi-computer execution, session branching, and long-running autonomous development workflows.
application
An experimental mathematical reasoning platform connecting ideas, Lean 4 formal proofs, theorem libraries, and AI agents.
- Exploring machine-checked mathematical reasoning and proof-assisted AI research.
- Developing agent-friendly interfaces for theorem exploration, proof construction, and verification.
open source
Tool Package Manager for AI Agents. Discovers, validates, and exposes npm packages as tools through MCP, SDKs, and command-line interfaces.
- Automatic npm tool discovery and sandboxed Deno execution.
- MCP aggregation and agent tooling infrastructure.
- Platform for building, sharing, and extending AI agents.
open source
A semantic validation system for AI-generated code, using domain specifications to detect inconsistencies and implementation drift.
- Declarative domain specifications using entities, signals, measures, and rules.
- Schema, structure, and LLM-based domain validation with actionable feedback for coding agents.
open source
An adversarial research-paper replication engine that extracts scientific claims, constructs evidence graphs, runs independent checks, and records reproducibility verdicts.
- Processed the Kolmogorov-Arnold Networks paper: 102 claims extracted, 24 reproduced, and 3 contradicted.
- Combines LLM extraction, simulations, mathematical checks, and provenance through Donto.
application
An AI-powered Discord agent with 80+ tools, multi-database memory, code execution, and autonomous improvement workflows.
- Code execution across 42+ programming languages.
- Agent tooling for software development, communication, and GitHub-driven self-improvement.
open source
CLI for using language models to optimize functions, validate functional equivalence, and benchmark implementations across languages and providers.
- Supports JavaScript, TypeScript, Python, Rust, and Go.
- Includes automated verification, performance comparison, a terminal UI, and cost analysis.