Stars
Specula: An agentic tool for finding deep bugs in system code using TLA+
DeepSeek Harness: Everything is a Plugin.
Long-horizon agent control plane for durable, governed work across Codex, Claude Code, and other harnesses.
27 editorial diagram types for Claude Code. Self-contained HTML + SVG. No shadows, no Mermaid-slop.
Lean 4 kernel / 'external checker' written in Lean 4
Kavita is a fast, feature rich, cross platform reading server. Built with the goal of being a full solution for all your reading needs. Setup your own server and share your reading collection with …
Fast, efficient, battle-tested at Alibaba's scale. Hybrid architecture code review tool: deterministic pipelines + LLM Agent, precise line-level comments, built-in multi-language ruleset (NPE, thre…
learn LLM inference system on Apple Silicon for systems engineers: build a tiny vLLM + Qwen
《深入理解 AI Agent：设计原理与工程实践》（李博杰 著）开源主仓库：全书正文、编译版 PDF 与按章配套代码
Metaprogramming, verified meta-theory and implementation of Rocq in Rocq
A tool for creating and running Linux containers using lightweight virtual machines on a Mac. It is written in Swift, and optimized for Apple silicon.
Multi-engine SMT-based automatic model checker for safety properties of Lustre programs
A curated list of awesome symbolic execution resources including essential research papers, lectures, videos, and tools.
The Rocq Prover is an interactive theorem prover, or proof assistant. It provides a formal language to write mathematical definitions, executable algorithms and theorems together with an environmen…
An extremely fast Python linter and code formatter, written in Rust.
A Hardware Description Language based on the Rust Programming Language
Modern embedded framework, using Rust and async.
It's a New Kind of Wrapper for Exposing LLVM (Safely)