Stars
A tool for creating and running Linux containers using lightweight virtual machines on a Mac. It is written in Swift, and optimized for Apple silicon.
Multi-engine SMT-based automatic model checker for safety properties of Lustre programs
A curated list of awesome symbolic execution resources including essential research papers, lectures, videos, and tools.
The Rocq Prover is an interactive theorem prover, or proof assistant. It provides a formal language to write mathematical definitions, executable algorithms and theorems together with an environmen…
An extremely fast Python linter and code formatter, written in Rust.
A Hardware Description Language based on the Rust Programming Language
Modern embedded framework, using Rust and async.
It's a New Kind of Wrapper for Exposing LLVM (Safely)
Project N.O.M.A.D, is a self-contained, offline survival computer packed with critical tools, knowledge, and AI to keep you informed and empowered—anytime, anywhere.
Dafny is a verification-aware programming language
A modern static site generator by the Material for MkDocs team
Symbolic execution tool for Sail ISA specifications
A fast RISC-V emulator based on the RISC-V Sail model, and an experimental ARM one
An analysis tool for Python that blurs the line between testing and type systems.
F´ - A flight software and embedded systems framework
A Lean formalisation of Maryna Viazovska's Fields Medal-winning solution to the sphere packing problem in dimension 8.
A comprehensive benchmark for AI-aided chip design
A type-safe, formally verifiable HDL compiler in Lean 4. Inspired by Clash, built for high-assurance hardware synthesis.