Skip to content

@verse-lab Verified Systems Engineering Lab

Change the repository type filter

All

    Repositories list

    37 repositories

    • loom2

      Public
      There is always loom for family.
      Lean
      •3•3•4•4•Updated Jun 11, 2026Jun 11, 2026

    • ego

      Public
      EGraphs in OCaml
      ocamlequality-saturationegraphs
      ocamlequality-saturationegraphs
      OCaml
      •
      GNU General Public License v3.0
      •10•82•3•0•Updated Jun 10, 2026Jun 10, 2026

    • lean-smt

      Public
      Tactics for discharging Lean goals into SMT solvers.
      Lean
      •
      Apache License 2.0
      •42•0•0•0•Updated Jun 6, 2026Jun 6, 2026

    • veil

      Public
      A verifier for automated and interactive proofs about transition systems.
      verificationproof-assistantlean
      verificationproof-assistantleansmt
      Lean
      •
      Apache License 2.0
      •16•253•2•1•Updated Jun 3, 2026Jun 3, 2026

    • Lentil

      Public
      (at least a useful portion of) Temporal Logic of Actions, a.k.a. TLA in Lean 4
      temporal-logic
      temporal-logic
      Lean
      •
      Apache License 2.0
      •0•22•0•0•Updated May 29, 2026May 29, 2026

    • yolo

      Public
      Lazy Proof Automation for Separation Logic
      Lean
      •0•0•0•0•Updated May 25, 2026May 25, 2026

    • lean4web

      Public
      Lean web editor
      TypeScript
      •
      Apache License 2.0
      •55•0•0•0•Updated May 8, 2026May 8, 2026

    • loom

      Public
      Loom is a framework for automated generation of foundational multi-modal verifiers. This repository is a mirror with stable snapshots. Submit issues and PRs her…
      Lean
      •
      Apache License 2.0
      •9•148•9•2•Updated May 8, 2026May 8, 2026

    • velvet

      Public
      An auto-active verifier embedded into Lean
      leandafny
      leandafny
      Lean
      •
      Apache License 2.0
      •3•55•0•0•Updated Apr 19, 2026Apr 19, 2026

    • greta

      Public
      This project demonstrates a grammar repair framework.
      OCaml
      •
      MIT License
      •0•5•0•0•Updated Mar 5, 2026Mar 5, 2026

    • lean-ssr

      Public
      LeanSSR: an SSReflect-Like Tactic Language for Lean
      Lean
      •
      Apache License 2.0
      •1•43•12•1•Updated Feb 14, 2026Feb 14, 2026

    • veil-usage-example

      Public template
      A template repository with an example of using Veil verifier as a Lean library.
      verificationleansmt
      verificationleansmt
      Lean
      •0•4•0•0•Updated Feb 12, 2026Feb 12, 2026

    • splean

      Public
      Separation Logic Proofs in Lean
      Lean
      •
      Apache License 2.0
      •6•52•0•0•Updated Jan 28, 2026Jan 28, 2026

    • ProofWidgets4

      Public
      Helper toolkit for creating your own Lean 4 UserWidgets
      Lean
      •
      Apache License 2.0
      •45•1•0•0•Updated Jan 3, 2026Jan 3, 2026

    • python-lean-vibe

      Public
      Experiment porting lambda-py to Lean with Claude Code
      Lean
      •0•0•0•0•Updated Dec 22, 2025Dec 22, 2025

    • FORCE

      Public
      C++
      •
      MIT License
      •1•0•0•0•Updated Sep 18, 2025Sep 18, 2025

    • intellij-rust

      Public archive
      Rust plugin for the IntelliJ Platform
      Kotlin
      •
      MIT License
      •0•1•0•0•Updated Aug 7, 2025Aug 7, 2025

    • doppler

      Public
      artifact of doppler
      LLVM
      •
      Apache License 2.0
      •0•3•0•0•Updated Mar 21, 2025Mar 21, 2025

    • z3

      Public
      The Z3 Theorem Prover
      C++
      •
      Other
      •1.7k•0•0•0•Updated Nov 25, 2024Nov 25, 2024

    • cleango

      Public
      Bindings to libclingo for the lean4 prover and programming language!
      C
      •1•1•0•0•Updated Nov 13, 2024Nov 13, 2024

    • obatcher_ds

      Public
      Jupyter Notebook
      •1•20•0•1•Updated Aug 29, 2024Aug 29, 2024

    • batcher-in-rust

      Public
      Rust
      •1•4•0•0•Updated Aug 27, 2024Aug 27, 2024

    • bythos

      Public
      Compositional Verification of Composite Byzantine Protocols
      distributed-systemscoqformal-verification
      distributed-systemscoqformal-verificationbyzantine-fault-tolerancedistributed-protocols
      Coq
      •
      BSD 2-Clause "Simplified" License
      •1•13•0•0•Updated Aug 24, 2024Aug 24, 2024

    • coq-lgtm

      Public
      Framework for Hyper-safety proofs about structured data
      Coq
      •
      MIT License
      •1•3•0•0•Updated Jul 25, 2024Jul 25, 2024

    • obatcher

      Public
      Parallel Programming over Domains
      Jupyter Notebook
      •
      ISC License
      •32•2•0•1•Updated Jul 4, 2024Jul 4, 2024

    • arboreta

      Public
      Mechanised Reasoning about Array-Based Trees in Separation Logic
      coqformal-verificationseparation-logic
      coqformal-verificationseparation-logicvector-clockrosetreegeneric-treelogical-clockdata-race-detection
      Coq
      •
      BSD 2-Clause "Simplified" License
      •0•0•0•0•Updated Jan 6, 2024Jan 6, 2024

    • rem

      Public
      Contributing the `extract method` refactoring for Rust.
      Rust
      •
      BSD 2-Clause "Simplified" License
      •1•4•0•0•Updated Sep 18, 2023Sep 18, 2023

    • NUS-Racket

      Public
      The Racket of NUSketeers on the high seas
      Scheme
      •
      Other
      •690•1•0•0•Updated Jun 7, 2023Jun 7, 2023

    • sisyphus

      Public
      Mostly Automated Proof Repair for Verified Libraries
      ocamlcoqhigher-order-functions
      ocamlcoqhigher-order-functionsformal-verificationseparation-logicpldi-artifactcurry-howard-isomorphismproof-repairinvariant-inference
      OCaml
      •
      GNU Affero General Public License v3.0
      •1•16•10•0•Updated Jun 1, 2023Jun 1, 2023

    • BOPC

      Public
      Block Oriented Programming -- Compiler
      Python
      •34•2•0•0•Updated Jun 1, 2023Jun 1, 2023
    ProTip! When viewing an organization's repositories, you can use the props. filter to filter by custom property.