Lean formalization of selected lemmas from "Term Rewriting and All That"

Definitional implementation of Cedar language and utilities for DRT

Intuitive, type-safe expression quotations for Lean 4.

A model of the RISC Zero zkVM and ecosystem in the Lean 4 Theorem Prover

Haskell bindings to the SDL2 library

SDL2 bindings for lean

The "batteries included" extended library for the Lean programming language and theorem prover

Examples of code verification using CBMC

Cryptographic Computing for Clean Rooms (C3R) encryption client and SDK

A Haskell library making it easier to write Alex lexers.

This project contains various supporting libraries for lean to reason about protocols.

Cryptol: The Language of Cryptography

PX4 Autopilot Software

Formal specification and verification of hardware, especially for security and privacy.

A mechanisation of Wasm in Coq(Rocq)

A model of the WebAssembly language in Redex

A mechanisation of Wasm in Isabelle.

Some benchmarks of different languages

A work in progress proof checker for LRAT files written in Lean.

Lean 4 programming language and theorem prover

Rich is a Python library for rich text and beautiful formatting in the terminal.

High Assurance Controller of Self-balancing Robot

Cache dependencies and build outputs in GitHub Actions

Semantics of x86-64 in K

A Tufte-inspired LaTeX class for producing handouts, papers, and books

Convert Haskell source code to Coq source code

A tool for analyzing x86-64 binaries.

A translation verifier for Reopt (https://github.com/GaloisInc/reopt)