Agda-style equational reasoning in Haskell

OmX - Oh My codeX: Your codex is not alone. Add hooks, agent teams, HUDs, and so much more.

A collection of notes I made during OPLSS25.

Cubical Type Theory in Scala 3 — port of Mortberg's cubicaltt

Claude Code is an agentic coding tool that lives in your terminal, understands your codebase, and helps you code faster by executing routine tasks, explaining complex code, and handling git workflo…

The open source coding agent.

AI Agent Assistant that integrates lots of IM platforms, LLMs, plugins and AI feature, and can be your openclaw alternative. ✨

Metaprogramming, verified meta-theory and implementation of Rocq in Rocq

Turn GitHub Copilot into OpenAI/Anthropic API compatible server. Usable with Claude Code!

Your own personal AI assistant. Any OS. Any Platform. The lobster way. 🦞

A Bowtie for a Beast (Artifact)

Coq formalization for Taming the Merge Operator

Java for Rust

A library of mechanised undecidability proofs in the Coq proof assistant.

Mathlib search tool

A project to digitalise results from physics into Lean.

Visual Studio Code extension for Coq

Cartesian Cubical Type Theory

Experimental implementation of Cubical Type Theory

Neon lights in the night tonight and stars that shine in the open sky

Formal verification tool for Rust: check 100% of execution cases of your programs to make safer applications.

Minimal implementations for dependent type checking and elaboration

An experimental library for Cubical Agda

LLMs as Copilots for Theorem Proving in Lean