Velisarios
Fault-tolerant system verifier
A framework for verifying the correctness of Byzantine fault-tolerant distributed systems
A Coq-based framework to verify the correctness of Byzantine fault-tolerant distributed systems
28 stars
3 watching
5 forks
Language: Coq
last commit: over 5 years ago Related projects:
| Repository | Description | Stars |
|---|---|---|
 uwplse/verdi | A framework for formally verifying distributed systems implementations in Coq. | 589 |
 mit-pdos/perennial | A system for verifying correctness of concurrent and crash-safe systems with recovery procedures | 163 |
 ymherklotz/vericert | A tool for formally verifying high-level synthesis of digital circuits | 88 |
 chipsalliance/verible | Develops a system for parsing and analyzing SystemVerilog code to improve developer productivity and ensure style compliance. | 1,380 |
 angelognazzo/reliable-trustworthy-ai | An implementation of a DeepPoly-based verifier for robustness analysis in deep neural networks | 1 |
 khronosgroup/vulkan-validationlayers | A set of tools to help developers verify correct use of the Vulkan API and detect potential errors in their applications. | 770 |
 frederikvigen/concert | A framework for verifying smart contracts in Coq to ensure their correctness and security | 0 |
 verinum/vcfloat | A unified framework for verifying C programs with floating-point computations using Coq | 24 |
 siimplex/concert | A framework for verifying smart contracts in Coq | 1 |
 coq-community/chapar | A framework for verifying causal consistency in distributed key-value stores and their clients using the Coq proof assistant | 32 |
 symbioticeda/riscv-formal | A framework for formally verifying RISC-V processors by providing a processor-independent formal description and testbenches. | 585 |
 vellvm/vellvm | A formal verification project of the LLVM compiler's semantics using Coq proof assistant. | 400 |
 valida-xyz/valida | A virtual machine for efficient and modular verification of program executions using Stark-based verification methods. | 290 |
 bedrocksystems/brick | Formalization of C++ logic for verifying concurrent programming | 69 |
 pirapira/evmverif | A framework for verifying smart contract code on the Ethereum Virtual Machine | 44 |