A formally verified security module for AMD confidential VMs

Dafny is a verification-aware programming language

The People's Verification System

The Z3 Theorem Prover

Working code samples for the blog post series: Introduction to hypothesis testing

Verified Rust for low-level systems code

Libraries useful for Dafny programs

Verifying encodings into propositional logic in Lean

Verifying OpenTitan

BLISS: Bimodal Lattice Signature Schemes

Clean, portable, tested implementations of post-quantum cryptography

Implementations of a fast Message-Authentication Code

A verified high-performance file system

Language for high-assurance and high-speed cryptography

Verified Assembly Language for Everest

A simple, reference implementation of a B^e-tree

OpenTitan: Open source silicon root of trust

LR(1) parser generator for Rust

Empowering everyone to build reliable and efficient software.

The WebAssembly Binary Toolkit

😎 Curated list of awesome things regarding the WebAssembly (wasm) ecosystem.