Pinned Repositories
bbv
Bedrock Bit Vector Library
bignums
Coq library of arbitrary large numbers. Provides BigN, BigZ, BigQ that used to be part of Coq standard library
bincat
Binary code static analyser, with IDA integration. Performs value and taint analysis, type reconstruction.
codegen
Coq plugin for monomorphization and C code generation
CompCert
The CompCert formally-verified C compiler
coq
Coq is a formal proof management system. It provides a formal language to write mathematical definitions, executable algorithms and theorems together with an environment for semi-interactive development of machine-checked proofs.
coq-elpi
Coq plugin embedding elpi
coqprime
Prime numbers for Coq
coqutil
Coq library for tactics, basic definitions, sets, maps
opam-repository
Main public package repository for OPAM, the source package manager of OCaml.
fajb's Repositories
fajb/opam-repository
Main public package repository for OPAM, the source package manager of OCaml.
fajb/bbv
Bedrock Bit Vector Library
fajb/bignums
Coq library of arbitrary large numbers. Provides BigN, BigZ, BigQ that used to be part of Coq standard library
fajb/bincat
Binary code static analyser, with IDA integration. Performs value and taint analysis, type reconstruction.
fajb/codegen
Coq plugin for monomorphization and C code generation
fajb/CompCert
The CompCert formally-verified C compiler
fajb/coq
Coq is a formal proof management system. It provides a formal language to write mathematical definitions, executable algorithms and theorems together with an environment for semi-interactive development of machine-checked proofs.
fajb/coq-elpi
Coq plugin embedding elpi
fajb/coqprime
Prime numbers for Coq
fajb/coqutil
Coq library for tactics, basic definitions, sets, maps
fajb/cross-crypto
Connecting computational and symbolic crypto models
fajb/fcf
Foundational Cryptography Framework for machine-checked proofs of cryptography.
fajb/fiat-crypto
Cryptographic Primitive Code Generation by Fiat
fajb/hash-consing-coq
fajb/jasmin
Jasmin compiler
fajb/kami
A Platform for High-Level Parametric Hardware Specification and its Modular Verification
fajb/llvm-project
The LLVM Project is a collection of modular and reusable compiler and toolchain technologies. Note: the repository does not accept github pull requests at this moment. Please submit your patches at http://reviews.llvm.org.
fajb/mczify
fajb/mythril
A hypervisor written in rust
fajb/opam-coq-archive
Archive for all Coq related OPAM packages organized in various repositories
fajb/RIOT
RIOT - The friendly OS for IoT
fajb/verdi
A framework for formally verifying distributed systems implementations in Coq
fajb/verdi-raft
An implementation of the Raft distributed consensus protocol, verified in Coq using the Verdi framework
fajb/VST
Verified Software Toolchain