An experimental proof assistant based on a type theory for synthetic ∞-categories.

Domain-Specific Languages of Mathematics

Verify Cairo contracts in Lean 4

Query compiler for secure multi-party computation.

Development environment for the Partisia Blockchain, made for creating applications and smart contracts.

Coordination repository for the Secure Code Working Group

Verified Rust for low-level systems code

Two-Level Type Theory

An experimental library for Cubical Agda

Automated property based testing for Rust (with shrinking).

A pure-Rust implementation of Bulletproofs using Ristretto.

Dafny is a verification-aware programming language

The main concordium node implementation.

A formalization of a Proof-of-Stake Nakamoto-style blockchain in Coq

Extracting Futhark code from the Coq proof assistant

A formalization of synthetic differential geometry in Coq using infinitesimal analysis

A framework for smart contract verification in Coq

Some scripts to help construct small reproducing examples of bugs, implement [Proof using], etc.

Python bindings for the Coq interactive proof assistant

Alpha-Structural Induction and Recursion for the Lambda Calculus in Constructive Type Theory

Exploring connections between automatic differentiation and smooth infinitesimal analysis, or smooth algebras

Master's Thesis working folder

Intuitionistic S5 logic formalization

Communication between Coq and SAT/SMT solvers

Rocq plugin embedding Elpi

Coq formalizations of functional languages.

Sokoban implementation in lean for proving solvability / unsolvability

Koka language compiler and interpreter