Receive and process logs from the Linux kernel.

A Virtual FIDO2 USB Device

Nix build hook that forwards remote builds to job schedulers.

Recognize cpu instructions in an arbitrary binary file

Applications for reverse engineering architecture 8051 firmware

Tool for talking to ITE ECs via SMBus debug interface (DBGR/SMB)

Windows kernel debugger for Linux hosts running Windows under KVM/QEMU

magic-trace collects and displays high-resolution traces of what a process is doing

Forward over Wormhole: streams over magic-wormhole Dilation connections

Python lib for Factur-X, the e-invoicing standard for France and Germany

AIA chasing through OpenSSL for TLS certificate chain building and verifying

The canonical spec for ulid

🛡️ Windows Hello™ style facial authentication for Linux

Security test suite for electronic invoices

Google OEM IPMI Commands expected for Host Stack

LLVM IR in natural Rust data structures

Crowdsourced tool for locating and reporting ALPRs

Manipulate LLVM-IR in Pure Rust

Cuq: A MIR-to-Coq Framework Targeting PTX for Formal Semantics and Verified Translation of Rust GPU Kernels

Loom is a framework for automated generation of foundational multi-modal verifiers. This repository is a mirror with stable snapshots. Submit issues and PRs here.

Terminal-based data visualization library for Lean 4. Port of Granite (Haskell) with type-safe guarantees. Create beautiful charts using Unicode braille characters.

Lean 4 port of Iris, a higher-order concurrent separation logic framework

Floating Point Semantics Mechanization for Lean

Eurisko-Inspired Discovery System for Lean in Lean

Formally Verified Arguments of Knowledge in Lean

Verified efficient algorithms in Lean4.