Visual Studio Code Extension and Language Server Protocol for Coq

Randomized Property-Based Testing Plugin for Coq

A complete proof in Agda of the Church-Rosser theorem for untyped λ-calculus formalizing the methods by Komori-Matsuda-Yamakawa (2014) and the proof by Nagele-van Oostrom-Sternagel (2016); reuses t…

Convert Haskell source code to Coq source code

A curated list of combinators

An AI Hedge Fund Team

⚙️ A curated list of static analysis (SAST) tools and linters for all programming languages, config files, build tools, and more. The focus is on tools which improve code quality.

A multi-programming language benchmark for LLMs

🙌 OpenHands: Code Less, Make More

codellm-devkit provides unified language to get off-the-shelf static analysis for multiple programming languages and support for applying those analyses for code LLM use cases.

Python client for coq-lsp

Deep Learning and Logical Reasoning from Data and Knowledge

Benchmark for evaluating Coq proof search tools.

A formalisation of the Calculus of Constructions

An encoding of Zermelo-Fraenkel Set Theory in Coq

Language models for Coq based on data collected from the coq lsp.

Statements of famous theorems proven in Coq [maintainer=@jmadiot]

Program Analisys and Transformation survey and links (particular focus on SSA)

ProbLog is a Probabilistic Logic Programming Language for logic programs with probabilities.

An API standard for single-agent reinforcement learning environments, with popular reference environments and related utilities (formerly Gym)

Python SDK, Proxy Server (LLM Gateway) to call 100+ LLM APIs in OpenAI format - [Bedrock, Azure, OpenAI, VertexAI, Cohere, Anthropic, Sagemaker, HuggingFace, Replicate, Groq]

Hypothesis is a powerful, flexible, and easy to use library for property-based testing.

Clover: Closed-Loop Verifiable Code Generation

VeriFFI: Verified Foreign Function Interface for connecting Coq programs to C programs at the operational and specification/verification levels; part of CertiCoq project

CoqHammer: An Automated Reasoning Hammer Tool for Coq - Proof Automation for Dependent Type Theory

Code for the paper LEGO-Prover: Neural Theorem Proving with Growing Libraries

COPRA: An in-COntext PRoof Agent which uses LLMs like GPTs to prove theorems in formal languages.

DIversity in VerificAtion

Long Range Arena for Benchmarking Efficient Transformers