Example code for the research paper "Masked Software Occlusion Culling"; implements an efficient alternative to the hierarchical depth buffer algorithm.

Open-source symbolic execution framework: https://maat.re

Grey-box Concolic Testing on Binary Code (ICSE '19)

FairFuzz: AFL extension targeting rare branches

A collection of fuzzers in a harness for testing the SpiderMonkey JavaScript engine.

Quake GPL Source Release

New idTech 4 engine with virtual texturing, CaS, GLSL, Radiant.NET and more!

BLOPS Open Source Reimplementation

100% Open Source CSGO

COD4 Open Source Reimplementation

Liberating Libraries through Automated Fuzz Driver Generation: Striking a Balance Without Consumer Code

LeanHammer is an automated reasoning tool for Lean that brings together multiple proof search and reconstruction techniques and combines them into one tool.

A Lean tactic for Canonical, a search procedure for terms in dependent type theory.

AI agents running research on single-GPU nanochat training automatically

Skills, MCP servers, Custom Agents, Agents.md for SDKs to ground Coding Agents

Trail of Bits Claude Code skills for security research, vulnerability detection, and audit workflows

An agentic skills framework & software development methodology that works.

Skills Catalog for Codex

Public repository for Agent Skills

A single CLAUDE.md file to improve Claude Code behavior, derived from Andrej Karpathy's observations on LLM coding pitfalls.

🪨 why use many token when few token do trick — Claude Code skill that cuts 65% of tokens by talking like caveman

L5 is a fun, fast, cross-platform, and lightweight implementation of the Processing API in Lua.

solver for the reachability modulo theories problem

Memory Manager For Small(ish) Microprocessors

Software model checking via exists-forall solving

Automated Reasoning Infrastructure & Applications

LLVM-based Static Analysis Framework

A language for constraint-guided and efficient LLM programming.