The agent harness performance optimization system. Skills, instincts, memory, security, and research-first development for Claude Code, Codex, Opencode, Cursor and beyond.

A powerful MCP toolkit for coding, providing semantic retrieval and editing capabilities - the IDE for your agent

The most comprehensive Claude Code guide: agentic workflows, hooks, skills, MCP servers, quizzes, and production-ready templates. 430K+ lines.

Nsight Python is a Python kernel profiling interface based on NVIDIA Nsight Tools

Lean formalization of selected lemmas from "Term Rewriting and All That"

Definitional implementation of Cedar language and utilities for DRT

Intuitive, type-safe expression quotations for Lean 4.

A model of the RISC Zero zkVM and ecosystem in the Lean 4 Theorem Prover

Haskell bindings to the SDL2 library

SDL2 bindings for lean

The "batteries included" extended library for the Lean programming language and theorem prover

Examples of code verification using CBMC

Cryptographic Computing for Clean Rooms (C3R) encryption client and SDK

A Haskell library making it easier to write Alex lexers.

This project contains various supporting libraries for lean to reason about protocols.

Cryptol: The Language of Cryptography

PX4 Autopilot Software

Formal specification and verification of hardware, especially for security and privacy.

A mechanisation of Wasm in Rocq

A model of the WebAssembly language in Redex

A mechanisation of Wasm in Isabelle.

Some benchmarks of different languages

A work in progress proof checker for LRAT files written in Lean.

Lean 4 programming language and theorem prover

Rich is a Python library for rich text and beautiful formatting in the terminal.

High Assurance Controller of Self-balancing Robot

Cache dependencies and build outputs in GitHub Actions

Semantics of x86-64 in K