Stars
TxHDL: a hardware description language that is a Rust library, proven on hardware. Read-only mirror; the work is done on the hdlfactory forge, https://git.hdlfactory.com/HDL/txhdl
Development repo for translating Software Foundations to Lean
A blazingly fast multi-language serialization framework for idiomatic domain objects, schema IDL, and cross-language data exchange.
Lean 4 + the Sail-generated RISC-V ISA model prove, CompCert-style, that an inductive WHILE semantics abstracts a real interpreter binary — zero sorries, zero axioms
Definitional implementation of Cedar language and utilities for DRT
A verifier for automated and interactive proofs about transition systems.
Pono: A flexible and extensible SMT-based model checker
The ripgrep of AI context: a zero-dependency C++23 CLI + MCP server for coding agents. Find what you want without reading the repo, then check you built what you meant — blast radius, tests-to-run,…
Specula: An agentic tool for finding deep bugs in system code using TLA+
DeepSeek Harness: Everything is a Plugin.
Turn long-horizon goals into verifiable results. A local-first semantic control plane and research workbench for long-running agent teams, across sessions and runtimes.
Editorial diagram design for Claude Code, Codex, GitHub Copilot, Cursor, Factory Droid, Qoder, and Pi. 45 diagram types. 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 …
Secure, 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 (N…
69A6 learn LLM inference system on Apple Silicon for systems engineers: build a tiny vLLM + Qwen
《深入理解 AI Agent：设计原理与工程实践》（李博杰 著）开源主仓库：全书正文、编译版 PDF 与按章配套代码