Creator · 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.
Creator · 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.
Creator · 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.
Creator · application
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.
Creator · 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.
Co-Founder · application
An international directory of civilian drone and UAV operators for hire: aerial photography and video, mapping, surveying, precision agriculture, inspections and infrared imaging. Built with Backbone.js, Node.js and Postgres.
- Over 200,000 visitors to the site and blog in 2014.