Starred repositories
Implementation of the Cedar Policy Language
Wasm interpreter in lean, designed for reasoning
Definitional implementation of Cedar language and utilities for DRT
Lean 4 port of Iris, a higher-order concurrent separation logic framework
Lean 4 programming language and theorem prover
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.
Canonical sources for HOL4 theorem-proving system. Branch develop is where “mainline development” occurs; when develop passes our regression tests, master is merged forward to catch up.
Creusot helps you prove your Rust code is correct.
An executable specification language with delightful tooling based on the temporal logic of actions (TLA)
Assured confidential execution (ACE) implements VM-based trusted execution environment (TEE) for embedded RISC-V systems with focus on a formally verified and auditable firmware.
Metaprogramming, verified meta-theory and implementation of Rocq in Rocq
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…
A collection of TLA⁺ specifications of varying complexities.
A precise specification for "Rust lite / MIR plus"
A BLE Heart Rate Monitor bridge for Social VR, OBS, Data Logging, and more!
Prove functional correctness of Ethereum smart contracts in higher-order logic
model-checking / verify-rust-std
Forked from rust-lang/rustVerifying the Rust standard library
TLC is a model checker for specifications written in TLA+. The TLA+Toolbox is an IDE for TLA+.
Repository moved to: https://codeberg.org/OpenTracksApp/OpenTracks
A curated list of awesome warez and piracy links.
Text page dewarping using a "cubic sheet" model