Verification of GoJournal

Concurrency Control Benchmark

Yet another YCSB workload generator in Rust.

Yahoo! Cloud Serving Benchmark

This is the public release of the ffwd delegation system, and associated benchmarks from the SOSP'17 paper.

Verifying concurrent storage and distributed systems

Proofs of distributed systems using Grove

An open-source AI agent that brings the power of Gemini directly into your terminal.

Multicore in-memory storage engine

Facebook AI Research Sequence-to-Sequence Toolkit written in Python.

自动同步 mihomo 内核、sing-box 内核、sing-box reF1nd 版内核和 Android 安装包、Dashboard 面板和 AdGuard Home 最新版

A platform for building proxies to bypass network restrictions.

Visual Studio Code extension for Coq

本仓库包含上海交通大学IPADS实验室设计的操作系统课程系列实验，以及前置课程ICS/CSAPP的系列实验。

DaisyNFS is an NFS server verified using Dafny and Perennial.

The Z3 Theorem Prover

Rust bindings for the Z3 solver.

Asterinas is a secure, fast, and general-purpose OS kernel, written in Rust and providing Linux-compatible ABI.

Verified KVM on Arm Relaxed Memory Hardware

A formally verified security module for AMD confidential VMs

A community preview of ongoing formal verification efforts for Asterinas

Peking University Undergraduate Thesis Template.

Asterinas is a secure, fast, and general-purpose OS kernel, written in Rust and providing Linux-compatible ABI.