Stars
an open source, extensible AI agent that goes beyond code suggestions - install, execute, edit, and test with any LLM
Programming language and compiler for spatial dataflow architectures, such as Cerebras WSE.
GeoPackage reader/writer built on top of rusqlite.
A collection of numeric types and traits for Rust.
Formally Verified Arguments of Knowledge in Lean
Formally Verified Float Implementation with lean4
tools and benchmarks for verified coding
Formal verification of Rust code with AI-assisted specification and proof.
A type-safe, formally verifiable HDL compiler in Lean 4. Inspired by Clash, built for high-assurance hardware synthesis.
Verified GPU programming framework for Lean 4. Write type-safe WebGPU shaders with formal verification, hardware-accelerated matrix ops, and cross-platform support (Metal/Vulkan/D3D12). Build prova…
Use Lean4 to build and train image recognition networks in MLIR.
Reactive notebook environment for Rust that uses standard .rs files. Features process isolation, hot reloading, and instant compilation via Cranelift.
q2 is the experimental implementation of Quarto 2 in Rust.
Interactive map of Switzerland's hydrological network
Lean 4 JSON Schema library — types, validation, correctness proofs, and deriving handlers
Typesetting and static site engine based on Typst
Radix: verified embedded DSL for high-performance applications
A fast, lightweight terminal-based spreadsheet application built in Rust with full formula support, cell references, and keyboard-driven navigation - perfect for command-line workflows.