Skip to content

@BasisResearch Basis Research Institute

All

    Repositories list

    47 repositories

    • verus

      Public
      Verified Rust for low-level systems code
      Rust
      •
      MIT License
      •232•0•3•3•Updated Oct 7, 2026Oct 7, 2026

    • dynestyx

      Public
      Probabilistic programming for dynamical systems! Supports models with NumPyro, deterministic & stochastic systems, discrete- and continuous-time systems, and mo…
      Python
      •
      Apache License 2.0
      •14•82•50•10•Updated Oct 7, 2026Oct 7, 2026

    • ship-your-ocaml

      Public
      Verifying OCaml's bootstrap compiler: bare-metal ocamlrun on the Sail RISC-V model, ZINC bytecode semantics, Lean 4 + iris-lean (plan, validation, scaffold)
      Lean
      •0•1•0•0•Updated Oct 7, 2026Oct 7, 2026

    • paralean

      Public
      Design and formal verification for distributed Lean proof development
      Lean
      •0•0•0•0•Updated Oct 7, 2026Oct 7, 2026

    • ship-your-lua

      Public
      Verifying Lua 5.4 on bare-metal RV64 against a formal semantics, on the Sail RISC-V model, in Lean 4 + iris-lean
      Lean
      •0•0•0•0•Updated Oct 6, 2026Oct 6, 2026

    • effectful

      Public
      An experimental library for metaprogramming with algebraic effects and handlers
      Python
      •
      Apache License 2.0
      •4•55•59•29•Updated Oct 6, 2026Oct 6, 2026

    • collab-splats

      Public
      Package for deriving gaussian splats, meshes, and associated semantic features
      Python
      •
      Apache License 2.0
      •0•2•4•1•Updated Oct 6, 2026Oct 6, 2026

    • ship-your-interpreter

      Public
      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 a…
      theorem-provingleanformal-verification
      theorem-provingleanformal-verificationrisc-vsaillean4
      Lean
      •4•46•0•1•Updated Oct 5, 2026Oct 5, 2026

    • toydb

      Public
      Distributed SQL database in Rust, written as an educational project
      Rust
      •
      Apache License 2.0
      •623•0•0•2•Updated Oct 5, 2026Oct 5, 2026

    • vismatch

      Public
      Wrapper of 50+ image matching models with a unified interface
      Python
      •
      BSD 3-Clause "New" or "Revised" License
      •82•0•0•0•Updated Oct 4, 2026Oct 4, 2026

    • predicators

      Public
      Learning for effective and efficient bilevel planning
      Python
      •
      MIT License
      •31•19•6•11•Updated Oct 3, 2026Oct 3, 2026

    • empiric

      Public
      Project page for EMPIRIC: Experiment-Driven Learning of Residual World Models for Robot Planning
      HTML
      •0•0•0•0•Updated Oct 3, 2026Oct 3, 2026

    • cvc5

      Public
      cvc5 is an open-source automatic theorem prover for Satisfiability Modulo Theories (SMT) problems.
      SMT
      •
      Other
      •306•0•0•0•Updated Oct 2, 2026Oct 2, 2026

    • droid

      Public
      Distributed Robot Interaction Dataset.
      Jupyter Notebook
      •100•0•0•1•Updated Oct 1, 2026Oct 1, 2026

    • lean.py

      Public
      Easy bindings between Lean and Python.
      Python
      •
      Apache License 2.0
      •2•36•0•1•Updated Sep 30, 2026Sep 30, 2026

    • tlaplus

      Public
      TLC is a model checker for specifications written in TLA+. The TLA+Toolbox is an IDE for TLA+.
      Java
      •
      MIT License
      •273•0•0•0•Updated Sep 24, 2026Sep 24, 2026

    • z3

      Public
      The Z3 Theorem Prover
      C++
      •
      Other
      •1.7k•0•0•0•Updated Sep 23, 2026Sep 23, 2026

    • verified-nrkernel

      Public
      Rust
      •
      Other
      •8•0•0•1•Updated Sep 16, 2026Sep 16, 2026

    • ansible-droid-panda-nuc

      Public
      Ansible playbook for setting up NUC to talk to libfranka emika robot
      0•0•0•0•Updated Aug 25, 2026Aug 25, 2026

    • fairo

      Public
      A modular embodied agent architecture and platform for building embodied agents
      Python
      •123•0•0•0•Updated Aug 18, 2026Aug 18, 2026

    • lean.rs

      Public
      Seamless Rust FFI bindings for Lean
      Lean
      •0•3•0•0•Updated Aug 17, 2026Aug 17, 2026

    • chirho

      Public
      An experimental language for causal reasoning
      Python
      •
      Apache License 2.0
      •22•278•74•8•Updated Jul 24, 2026Jul 24, 2026

    • verified-nftables

      Public
      A verified nftables bytecode compiler
      Rocq Prover
      •0•3•0•0•Updated Jul 22, 2026Jul 22, 2026

    • collab-environment

      Public
      Representing, modeling, and simulating behavior within naturalistic environments
      Jupyter Notebook
      •
      Apache License 2.0
      •0•2•8•3•Updated Jul 21, 2026Jul 21, 2026

    • wasserstein-residuals

      Public
      Python
      •
      Apache License 2.0
      •0•2•0•0•Updated Jul 21, 2026Jul 21, 2026

    • VeriDNS

      Public
      A RFC Compliant Verified DNS server
      Lean
      •1•13•0•0•Updated Jul 17, 2026Jul 17, 2026

    • Autumn.cpp

      Public
      Autumn.CPP (aka. Autumn.WASM) A cpp implementation of Autumn that compiles to WASM, Python and Julia bindings.
      interpreterprogramminglanguage
      interpreterprogramminglanguage
      C++
      •
      MIT License
      •3•10•0•0•Updated Jul 14, 2026Jul 14, 2026

    • verso

      Public
      Lean documentation authoring tool
      Lean
      •
      Apache License 2.0
      •124•0•0•0•Updated Jul 6, 2026Jul 6, 2026

    • LLM-Lang-Design-How-do-agents-use-languages

      Public
      An experiment on how agents use languages.
      C
      •0•0•0•0•Updated Jun 11, 2026Jun 11, 2026

    • realpbt-lean

      Public
      Experiments porting RealPBT to Lean via Crosshair.
      Python
      •
      Other
      •0•0•0•0•Updated May 29, 2026May 29, 2026
    ProTip! When viewing an organization's repositories, you can use the props. filter to filter by custom property.