We define a simple programming language, simp_lang, then instantiate Iris to verify simple simp_lang programs with concurrent separation logic.

A precise specification for "Rust lite / MIR plus"

A static verifier for Rust, based on the Viper verification infrastructure.

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

Fork to merge newest Boogie and Proof Generation

Boogie Proofgen

c# uabe for newer versions of unity

A static verifier for Rust, based on the Viper verification infrastructure.

Revive unavailable songs for Netease Cloud Music (Refactored & Enhanced version)

Goose converts a subset of Go to Rocq

Verifying concurrent storage and distributed systems

The CompCert formally-verified C compiler

Verified Rust for low-level systems code

Creusot helps you prove your code is correct in an automated fashion.

Course on Metaprogramming

CakeML: A Verified Implementation of ML

Download sheet music

The modding API for Stardew Valley.

Poly/ML

Avalonia-based .NET Decompiler (port of ILSpy)

A library for patching, replacing and decorating .NET and Mono methods during runtime

The HOL Light theorem prover

A fast and clever hex editor for macOS

Lean 4 programming language and theorem prover