A static site generator for data apps, dashboards, reports, and more. Observable Framework combines JavaScript on the front-end for interactive graphics with any language on the back-end for data a…

A dynamic language and bytecode vm

Tongyi Deep Research, the Leading Open-source Deep Research Agent

A controlled concurrency testing framework for the JVM

Framework for testing concurrent code on JVM languages

The Z3 Theorem Prover

Review-first terminal diff viewer for agentic coders

kiwi array programming language

Build production-ready applications in TypeScript

White-box automation for Lean 4

Firmware for the Xteink X3 and X4 e-paper display readers

Lean documentation authoring tool

Lightweight and declarative sandboxing for AI agents on Linux and macOS using Nix.

Various interesting articles, in PDF or PS form

Claude Code notifications without the context switch. A minimal, always-present session manager for macOS.

A framework for performing AI model inference on encrypted data.

A type-safe Haskell SQL library

A tool to extract gnark circuits defined in Go to Lean for formal verification.

The world's smallest AI agent runtime. 49KB. Written in Zig. Zero dependencies.

A binary and file access authorization system for macOS.

GNU Emacs / N Λ N O - Emacs made simple

Claude Code Emacs integration

A Linux based operating system hardened and purpose built for AI agents

A Lean 4.27 runtime in Rust

kdb+ production framework. Read the doc: https://dataintellecttech.github.io/TorQ/. Join the group!

An executable specification language with delightful tooling based on the temporal logic of actions (TLA)

Neovim support for the Lean theorem prover

Implementation of a quantum simulator using APL

Deployments of fancy cryptography