Snapkitty Collective LLC

Deterministic systems, verified end to end.

Alternative attention, SUBLEQ, integer computing, formal proofs and the hardware to run them, built in the open.

183models

13datasets

12spaces

10collections

37in the October drop

⭐ Start here: flagship releases Browse all 194 repositories October 2026 drop Latest paper

Featured release

New paper, with its Lean proofs and a reproducible axiom audit.

New paper October 2026 DOI 10.5281/zenodo.23287576

Conservation-Preserving Compilation for a 1+1D Lattice Shadow of φ⁴

Symmetries of the target Hamiltonian constrain circuit synthesis instead of filtering measured shots. Every admitted Trotter schedule is proved, in Lean 4, to commute with its mode's conserved operator, for every lattice size and every angle. Each emitted schedule carries a SHA-256 certificate.

Read the paper Lean proofs Code

$ lake build

Build completed successfully.

$ lake env lean Audit.lean

admitted_trotter_commutes

operator_commutation

emitted_commutes

depends on: propext,

Classical.choice, Quot.sound

no project axioms · no sorry

Research highlights

Releases with published evidence you can check.

Model · GGUFhilbert-4b-baseline-GGUFHilbert's 4B decision model as Q8_0 and Q4_K_M. Q8_0 matches BF16 on 99.3% of decisions, measured row by row.
Datasettoolgate-benchBenchmark for tool-call gating in LLM agents: accept, require approval or reject, with a frozen held-out split.
Model · v0.3.0snapkitty-nemotron-harnessFail-closed tool gate for local agents: 0% unsafe passes on ToolGate-Bench v1, about 24 µs per decision.
Modelsymbolic-morphologyLatin verb morphology from raw letters with hand-derived gradients and no ML framework, down to NAND gates.
  

Collections

Every repository belongs to one of 10 collections.

Models and TrainingLanguage models, fine-tune checkpoints, reward models and the training infrastructure behind them.21 repositories · 3 new Agents and OrchestrationMulti-agent systems, orchestration engines and autonomous execution frameworks with sealed audit trails.27 repositories · 2 new Formal VerificationMachine-checked proofs in Lean 4 and Agda, verified compilers and cross-language verification.24 repositories · 7 new GPU Kernels and HardwareCUDA kernels, synthesizable RTL accelerators, hardware operating systems and flight computers.17 repositories · 5 new Quantum Computing and PhysicsTopological quantum computing, quantum walks, the TLM/JXCL stack and black-hole physics.15 repositories · 3 new Compilers and RuntimesCompilers, virtual machines, emulators, runtime engines and purpose-built languages.21 repositories · 4 new Security and CryptographyCryptographic verification, attestation protocols, WORM audit chains, policy engines and on-chain work.17 repositories · 6 new Infrastructure and ToolsMCP servers, IDEs, browsers, harnesses and the developer tooling that runs the collective.25 repositories · 2 new Research and PapersPublished research, tournament results and open scholarship with traceable evidence.16 repositories · 3 new Community and CultureThe Saint Errant Digital Society, algorithmic art, open governance and SnapKitty culture.11 repositories · 2 new

Catalogue

All 194 repositories in one place, grouped by collection. Search by name, language or topic.

Run locally

snapkitty-merged: our merged Nemotron 4.2B as a 2.7 GB Q4_K_M GGUF with a 4,096-token context, for llama.cpp, Ollama and LM Studio.

ollama run hf.co/Snapkitty/snapkitty-merged:Q4_K_M

All GGUF models

Upstream contributors to Agda, the dependently typed proof assistant, and LiquidHaskell, refinement types for Haskell from the UC San Diego Programming Systems group.

Commercial license

SnapKitty code is open source, primarily under AGPL-3.0; each repository states its exact license on its card. A proprietary commercial license from Snapkitty Collective LLC lets you ship SnapKitty code without the AGPL's source-sharing and network-use obligations.

Get a commercial license