Shuttle is a library for testing concurrent Rust code

Verification tool for distributed protocols based on inductive proof decomposition.

Play/learn/work with me

A verification toolchain for Rust programs

Mathematical Components

slides for the book "Principles od Abstract Interpretation", P. Cousot, MIT Press, 2021

Yosys Open SYnthesis Suite

Sail architecture definition language

FPGA related files for ORAM

blueprint for prime number theorem and more

Path ORAM reference implementation

Path ORAM is a simple oblivious RAM algorithm. While using cloud platform or any other insecure memory, attack can be made using the access pattern. Oblivious RAM is the way to hide the memory acce…

Measures of distance between two probability density functions

A framework for the elicitation, specification, formalization and analysis of requirements.

A Probability Theory Library for the Coq Theorem Prover

Coq library for reasoning on randomized algorithms [maintainers=@anton-trunov,@volodeyka]

Verified hash-based AMQ structures in Coq

Inference Llama 2 in one file of pure C

EasyCrypt: Computer-Aided Cryptographic Proofs

A Language for Oblivious Computation

A set of Processing animations, which have commented code

RARS -- RISC-V Assembler and Runtime Simulator

Coq formalization of intuitionistic first-order logic

A cost-aware logical framework, embedded in Agda.

Label dependent dependent session types