-
lab-automation-observatory Public
Studying where lab automation work breaks
-
neuroai-workbench Public
Open-source reference implementation for NeuroAI Assessment Instrument and its controlled observatory workflow.
-
Compiles APIs, schemas, procedures, traces and expert decisions into typed, provenance-aware environment models and verifiable packs.
-
-
neuroai-observatory-data Public
Public canonical observatory data for NeuroAI Workbench
-
ts-mono Public
Forked from meridianlabs-ai/ts-monoTypeScript monorepo
TypeScript UpdatedSep 16, 2026 -
inspect_evals Public
Forked from UKGovernmentBEIS/inspect_evalsCollection of evals for Inspect AI
-
formal-proofs Public
Forked from starkware-libs/formal-proofsFormal verification of various aspects of the Cairo programming language using the Lean programming language and proof assistant.
Lean Apache License 2.0 UpdatedSep 5, 2026 -
ai-adoption-us Public
Studying how generative AI moves from work adoption into routine use, AI-assisted working time, and self-reported time savings in the United States.
-
mathlib4 Public
Forked from leanprover-community/mathlib4The math library of Lean 4
-
TauCeti Public
Forked from TauCetiProject/TauCetiAn AIs-welcome Lean library downstream of Mathlib: AI handle the implementation and review, humans write the roadmaps and review rubrics
-
OpenJarvis Public
Forked from open-jarvis/OpenJarvisPersonal AI, On Personal Devices
-
terminal-bench-1 Public
Forked from harbor-framework/terminal-benchMeasuring and evolving with the frontier of agent work
-
cslib Public
Forked from leanprover/cslibA Lean library for Computer Science
Lean Apache License 2.0 UpdatedAug 31, 2026 -
MathEvidence Public
Open computational evidence infrastructure for Lean - Turns external solver results into Lean-checked evidence through explicit contracts, replayable bundles, and untrusted computer-algebra adapters.
-
QSpecBench Public
A shared benchmark suite for checking quantum correctness claims.
-
lean-project-evidence Public
Lean Project Evidence (lpe) is a project-grounded evidence and review layer for AI-assisted Lean development.
-
open-verification-kernel Public
Open Verification Kernel (OVK) is an open-source, solver-agnostic verification layer for AI-agent engineering workflows.
-
ovk-consumer-express-actions Public
Independent OVK consumer gate: Express + GitHub Actions pinned to open-verification-kernel@v1.2.1
-
Independent OVK consumer gate: FastAPI + Terraform pinned to open-verification-kernel@v1.2.1
-
ens-grant-decision-integrity Public
ENS Grants Charter and machine-readable decision-record profile for reconstructable, human-authorized funding decisions.
-
verifierlab Public
Local-first campaigns for stress-testing graders, reward functions, and policy checkers under optimization pressure.
-
EVERYTHING-RINGS Public
EVERYTHING RINGS is a local-first acoustic instrument for estimating the audible resonances of struck physical objects, reconstructing those resonances, and turning them into playable instruments.
-
lean-endkan Public
Practical Automation for Ends, Coends, and Kan Extensions in Lean 4
-
lean-yo Public
A Lean 4 tactic library that simplifies category theory proofs using (co)Yoneda isomorphisms
-
lean-effects Public
Algebraic Effects via Lawvere Theories & Handlers with Code Generation, Fusion Theorems, and Curated Simp Packs
-
lean-cat-nf Public
Category Normal Form for Lean 4
-
lean-optics Public
Lean Optics provides an implementation of profunctor optics for Lean 4, featuring law-carrying composition, automated proof generation, and production-ready performance guarantees. Built on solid m…
-
lean-containers Public
lean-containers is a container library for Lean 4 that provides type-safe, mathematically rigorous implementations of container types and operations.
-
lean-uprove Public
A Lean 4 tactic for automating proofs involving universal properties in category theory