Verified compiler from LambdaBox to WebAssembly, C, Rust, and OCaml

Distributions of Agda executable compiled into WebAssembly.

Where we explore more interesting data types than just fixed points of polynomials

A collection of formalized statements of conjectures in Lean.

Haskell to C compiler via Categorifier

Interpret Haskell programs into any cartesian closed category.

Framework for generating constrained random data using a subset of first order logic

Refinement types + dependent types = ❤️

Verified Software Toolchain

Proposed extensions to Agda standard's library

Shallow embedding of Protocols using Agda dependent types

Formally Verified Arguments of Knowledge in Lean

Python library for automatic analysis of Ancient Greek hexameter. The algorithm uses linguistic rules and finite-state technology.

Libraries and command-line tools for metrical analysis of epic Greek hexameter

GUI file synchronization client that can sync with any cloud provider

Natural language tactics to teach mathematics using Lean 4

Mathematical terms, definitions, and propositions in as many languages as possible

Sound and complete validators (AIM XL talk)

Learn Lean 4 with PLFA proofs.

Automated Formal Verification Tool for Cardano Smart Contracts

The formally verified crypto library for Rust

An Agda mechanization of the Streamlet consensus protocol.

Formal specification of the Ouroboros Leios protocol variants