Pinned Repositories
crucible
Crucible is a library for symbolic simulation of imperative programs
cryptol
Cryptol: The Language of Cryptography
HaLVM
The Haskell Lightweight Virtual Machine (HaLVM): GHC running on Xen
haskell-tor
A Haskell implementation of the Tor protocol.
ivory
The Ivory EDSL
macaw
Open source binary analysis tools.
MATE
MATE is a suite of tools for interactive program analysis with a focus on hunting for bugs in C and C++ code using Code Property Graphs.
reopt
A tool for analyzing x86-64 binaries.
saw-script
The SAW scripting language.
swanky
A suite of rust libraries for secure multi-party computation
Galois, Inc.'s Repositories
GaloisInc/cryptol
Cryptol: The Language of Cryptography
GaloisInc/crucible
Crucible is a library for symbolic simulation of imperative programs
GaloisInc/saw-script
The SAW scripting language.
GaloisInc/swanky
A suite of rust libraries for secure multi-party computation
GaloisInc/macaw
Open source binary analysis tools.
GaloisInc/yapall
A precise and scalable pointer analysis for LLVM, written in Ascent
GaloisInc/parameterized-utils
A set of utilities for using indexed types including containers, equality, and comparison.
GaloisInc/cryptol-specs
A central repository for specifications of cryptographic algorithms in Cryptol
GaloisInc/llvm-pretty
An llvm pretty printer inspired by the haskell llvm binding
GaloisInc/json
Haskell JSON library
GaloisInc/HARDENS
Repository for the HARDENS project
GaloisInc/pate
Patches Assured up to Trace Equivalence
GaloisInc/cheesecloth
GaloisInc/macaw-loader
Uniform interface to load a binary executable and get Macaw Memory and a list of entry points.
GaloisInc/what4-solvers
Multi-platform binary creation for solvers of the versions most suitable for use with What4
GaloisInc/VERSE-Toolchain
Tools for testing and verifying the safety and correctness of C programs.
GaloisInc/ckzg-eip-4844-verification
GaloisInc/VERSE-OpenSUT
Open System Under Test (SUT) for the VERSE demonstrator
GaloisInc/cheesecloth-curve25519-dalek
GaloisInc/copilot-1
A stream-based runtime-verification framework for generating hard real-time C code.
GaloisInc/fret
A framework for the elicitation, specification, formalization and understanding of requirements.
GaloisInc/jolt
The simplest and most extensible zkVM. Fast and fully open source from a16z crypto and friends. ⚡
GaloisInc/lustre-w
A parser and AST for Lustre
GaloisInc/MicroRAM
GaloisInc/nixpkgs
Nix Packages collection & NixOS
GaloisInc/pono
Pono: A flexible and extensible SMT-based model checker
GaloisInc/proverbot9001
GaloisInc/scuttlebutt-attack
GaloisInc/ssb-handshake
GaloisInc/zk-lean
zkLean is a domain specific language (DSL) in Lean for specifying zero-knowledge statements