Skip to content

@GaloisInc Galois, Inc.

Change the repository type filter

All

    Repositories list

    515 repositories

    • crucible

      Public
      Crucible is a library for symbolic simulation of imperative programs
      Rust
      •42•693•171•5•Updated Feb 5, 2025Feb 5, 2025

    • what4

      Public
      Symbolic formula representation and solver interaction library
      Haskell
      •13•156•48•2•Updated Feb 5, 2025Feb 5, 2025

    • pate

      Public
      Patches Assured up to Trace Equivalence
      armstatic-analysisverificationbinary-analysispowerpccompositional-verification
      Haskell
      •
      Other
      •3•14•26•7•Updated Feb 5, 2025Feb 5, 2025

    • sail

      Public
      Sail architecture definition language
      Isabelle
      •
      Other
      •120•0•0•0•Updated Feb 5, 2025Feb 5, 2025

    • jolt

      Public
      The simplest and most extensible zkVM. Fast and fully open source from a16z crypto and friends. ⚡
      Rust
      •
      MIT License
      •197•0•0•0•Updated Feb 4, 2025Feb 4, 2025

    • cryptol-specs

      Public
      A central repository for specifications of cryptographic algorithms in Cryptol
      TeX
      •
      BSD 3-Clause "New" or "Revised" License
      •7•40•42•4•Updated Feb 4, 2025Feb 4, 2025

    • copilot-1

      Public
      A stream-based runtime-verification framework for generating hard real-time C code.
      Haskell
      •59•0•2•0•Updated Feb 4, 2025Feb 4, 2025

    • dlkoopman

      Public
      A general-purpose Python package for Koopman theory using deep learning.
      autoencoderdynamical-systemskoopmandeep-learning
      Python
      •
      MIT License
      •14•91•0•0•Updated Feb 4, 2025Feb 4, 2025

    • parameterized-utils

      Public
      A set of utilities for using indexed types including containers, equality, and comparison.
      Haskell
      •
      BSD 3-Clause "New" or "Revised" License
      •13•60•19•6•Updated Feb 4, 2025Feb 4, 2025

    • zk-lean

      Public
      zkLean is a domain specific language (DSL) in Lean for specifying zero-knowledge statements
      Lean
      •
      BSD 3-Clause "New" or "Revised" License
      •0•7•0•0•Updated Feb 4, 2025Feb 4, 2025

    • saw-script

      Public
      The SAW scripting language.
      Haskell
      •
      BSD 3-Clause "New" or "Revised" License
      •63•446•427•21•Updated Feb 3, 2025Feb 3, 2025

    • entree-specs

      Public
      Coq
      •
      BSD 3-Clause "New" or "Revised" License
      •0•2•3•0•Updated Feb 3, 2025Feb 3, 2025

    • cryptol

      Public
      Cryptol: The Language of Cryptography
      Haskell
      •
      BSD 3-Clause "New" or "Revised" License
      •123•1.1k•236•12•Updated Feb 3, 2025Feb 3, 2025

    • llvm-pretty-bc-parser

      Public
      Parser for the llvm bitcode format
      LLVM
      •
      Other
      •7•60•58•4•Updated Feb 3, 2025Feb 3, 2025

    • yapall

      Public
      A precise and scalable pointer analysis for LLVM, written in Ascent
      llvmstatic-analysisdatalogprogram-analysispointer-analysis
      C
      •
      BSD 3-Clause "New" or "Revised" License
      •3•62•14•6•Updated Feb 1, 2025Feb 1, 2025

    • VERSE-OpenSUT

      Public
      Open System Under Test (SUT) for the VERSE demonstrator
      C
      •
      BSD 3-Clause "New" or "Revised" License
      •0•2•41•4•Updated Jan 31, 2025Jan 31, 2025

    • cerberus

      Public
      Cerberus C semantics
      OCaml
      •
      Other
      •30•0•0•2•Updated Jan 31, 2025Jan 31, 2025

    • VERSE-Toolchain

      Public
      Tools for testing and verifying the safety and correctness of C programs.
      OCaml
      •
      BSD 3-Clause "New" or "Revised" License
      •1•6•60•4•Updated Jan 30, 2025Jan 30, 2025

    • cclyzerpp

      Public
      cclyzer++ is a precise and scalable pointer analysis for LLVM code.
      llvmstatic-analysisdatalogprogram-analysispointer-analysissouffle
      C++
      •
      BSD 3-Clause "New" or "Revised" License
      •14•138•26•0•Updated Jan 30, 2025Jan 30, 2025

    • pono

      Public
      Pono: A flexible and extensible SMT-based model checker
      C++
      •
      Other
      •31•0•0•0•Updated Jan 29, 2025Jan 29, 2025

    • BLST-Verification

      Public
      BLST-Verification
      Python
      •3•21•2•1•Updated Jan 29, 2025Jan 29, 2025

    • aws-lc-verification

      Public
      Go
      •
      Apache License 2.0
      •19•0•0•0•Updated Jan 27, 2025Jan 27, 2025

    • stubs

      Public
      Simple language for defining stub function semantics for binary analysis
      Haskell
      •
      BSD 3-Clause "New" or "Revised" License
      •0•2•10•0•Updated Jan 14, 2025Jan 14, 2025

    • language-rust

      Public
      Parser and pretty-printer for the Rust language
      Haskell
      •
      BSD 3-Clause "New" or "Revised" License
      •18•1•2•0•Updated Jan 10, 2025Jan 10, 2025

    • elf-edit

      Public
      The elf-edit library provides a datatype suitable for reading and writing Elf files.
      Haskell
      •
      Other
      •6•36•7•0•Updated Jan 8, 2025Jan 8, 2025

    • .github

      Public
      A collection of github actions and other tooling designed to reduce repetition and make adding pipelines easier.
      1•0•1•0•Updated Jan 7, 2025Jan 7, 2025

    • ckzg-eip-4844-verification

      Public
      Makefile
      •
      BSD 3-Clause "New" or "Revised" License
      •2•3•2•0•Updated Jan 7, 2025Jan 7, 2025

    • macaw

      Public
      Open source binary analysis tools.
      Haskell
      •
      BSD 3-Clause "New" or "Revised" License
      •20•211•71•3•Updated Jan 2, 2025Jan 2, 2025

    • macaw-loader

      Public
      Uniform interface to load a binary executable and get Macaw Memory and a list of entry points.
      Haskell
      •1•5•3•1•Updated Dec 20, 2024Dec 20, 2024

    • proverbot9001

      Public
      Coq
      •
      GNU General Public License v3.0
      •18•0•0•0•Updated Dec 19, 2024Dec 19, 2024