Lists (4)
Stars
Lean 4 proofs that libtommath v1.3.0 compiled for RV64I meets its specification on the Sail RISC-V model
💥 Blazing fast terminal file manager written in Rust, based on async I/O.
Language for high-assurance and high-speed cryptography
Packed arrays for scalar types in Lean 4
Algorithms and Complexity Library using the lightweight query combinator framework called "Prog"
Beta: The truly free, open-source, local-first, cross-platform video editor. Scriptable through a JSON-RPC API & MCP.
A Logical Relation for Martin-Löf Type Theory in Agda
On-demand commutation theorems for state operations in Lean 4: a simproc plus realizable constants, so only the pairs proofs use are ever proved
An external lean checker with a proof of consistency
Legacy Complexitylib V1; development continues at cslib-community/complexitylib.
Built-in exact decimal numbers for JavaScript
Lean certificates accompanying Navier-Stokes and Euler results
A PostgREST-inspired REST/GraphQL API for PostgreSQL, written in Rust
Nix tooling for the seL4 microkernel & ecosystem
FormalQualBench problem: ParisHarringtonPrinciple
EXPERIMENTAL: Kirby-Paris Theorem formalized in Lean 4