The Lean Computer Science Library (CSLib)

An embedding of Boogie semantics into Lean

A verified tensor library in Lean

Formalising the WASM spec in Lean

Experiments on automation for Lean

A toy ELF parser/validator

Interactive formal verification tool for Yul programs

SampCert : Verified Differential Privacy

Armv8 Native Code Symbolic Simulator in Lean

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

Application Binary Interface for the Arm® Architecture

The Z3 Theorem Prover

Python bindings to Ghidra's SLEIGH library for disassembly and lifting to P-Code IR

Sail x86 model automatically translated from the ACL2 model

ACL2 System and Books as Maintained by the Community

The HOL Light theorem prover

The X86 Encoder Decoder (XED), is a software library for encoding and decoding X86 (IA32 and Intel64) instructions

Implementation of Pedersen hash function in OCaml

RISC-V Instruction Set Manual

Spike, a RISC-V ISA Simulator

Database of CPU Opcodes

Original Apollo 11 Guidance Computer (AGC) source code for the command and lunar modules.

A book-in-progress about the Linux kernel and its insides.

Simple kernel-level programs to be verified using the ACL2-based x86isa reasoning framework

Shilpi's Fork of ACL2 System and Books

Papers from the computer science community to read and discuss.

FreeBSD src tree modified to support booting on an x86_64 model implemented in ACL2