Skip to content
@BasisResearch

Basis Research Institute

Basis builds reasoning engines that advance society's ability to solve intractable problems

Popular repositories Loading

  1. chirho chirho Public

    An experimental language for causal reasoning

    Python 281 22

  2. dynestyx dynestyx Public

    Probabilistic programming for dynamical systems! Supports models with NumPyro, deterministic & stochastic systems, discrete- and continuous-time systems, and more!

    Python 87 14

  3. ship-your-interpreter 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 axioms

    Lean 57 7

  4. effectful effectful Public

    An experimental library for metaprogramming with algebraic effects and handlers

    Python 55 4

  5. lean.py lean.py Public

    Easy bindings between Lean and Python.

    Python 37 2

  6. millipede millipede Public

    A library for bayesian variable selection

    Jupyter Notebook 33 5

Repositories

Showing 10 of 50 repositories
  • verified-libtommath Public

    Lean 4 proofs that libtommath v1.3.0 compiled for RV64I meets its specification on the Sail RISC-V model

    BasisResearch/verified-libtommath's past year of commit activity
    Lean 4 Apache-2.0 0 0 0 Updated Oct 31, 2026
  • dynestyx Public

    Probabilistic programming for dynamical systems! Supports models with NumPyro, deterministic & stochastic systems, discrete- and continuous-time systems, and more!

    BasisResearch/dynestyx's past year of commit activity
    Python 87 Apache-2.0 14 52 (3 issues need help) 9 Updated Oct 31, 2026
  • lean.py Public

    Easy bindings between Lean and Python.

    BasisResearch/lean.py's past year of commit activity
    Python 37 Apache-2.0 2 0 2 Updated Oct 31, 2026
  • paralean Public

    Design and formal verification for distributed Lean proof development

    BasisResearch/paralean's past year of commit activity
    Rust 0 0 0 0 Updated Oct 29, 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)

    BasisResearch/ship-your-ocaml's past year of commit activity
    Lean 2 0 0 0 Updated Oct 28, 2026
  • ship-your-tcc Public

    Ship your interpreter for tcc -run: TinyCC on Sail RV64I, a differential against CompCert and Certora's Lean Clight, and per-program end-to-end proofs

    BasisResearch/ship-your-tcc's past year of commit activity
    Lean 0 0 0 0 Updated Oct 28, 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

    BasisResearch/ship-your-lua's past year of commit activity
    Lean 3 0 0 0 Updated Oct 27, 2026
  • lean4-mlir Public Forked from brettkoonce/lean4-mlir

    Lean specification of neural architectures with verified GPU codegen.

    BasisResearch/lean4-mlir's past year of commit activity
    MLIR 0 BSD-3-Clause 5 0 1 Updated Oct 27, 2026
  • effectful Public

    An experimental library for metaprogramming with algebraic effects and handlers

    BasisResearch/effectful's past year of commit activity
    Python 55 Apache-2.0 4 60 (1 issue needs help) 32 Updated Oct 26, 2026
  • predicators Public Forked from Learning-and-Intelligent-Systems/predicators

    Learning for effective and efficient bilevel planning

    BasisResearch/predicators's past year of commit activity
    Python 24 MIT 32 6 72 Updated Oct 24, 2026
View all repositories

People

This organization has no public members. You must be a member to see who’s a part of this organization.

Most used topics

Loading…