2027QuantInternships
Public quant internship repository, maintained by NUFT but available for everyone.
aeneas
A verification toolchain for Rust programs
aesop
White-box automation for Lean 4
agda
Agda is a dependently typed programming language / interactive theorem prover.
analysis
A Lean companion to Analysis I
ArkLib
Formally Verified Arguments of Knowledge in Lean
batteries
The "batteries included" extended library for the Lean programming language and theorem prover
boringssl
Mirror of BoringSSL
catala
Programming language for literate programming law specification
cedille
Cedille, a dependently typed programming languages based on the Calculus of Dependent Lambda Eliminations
certigrad
Bug-free machine learning on stochastic computation graphs
codspeed
CodSpeed is the all-in-one performance testing toolkit. Optimize code performance and catch regressions early.
comparator
No description
cslib
The Lean Computer Science Library (CSLib)
data-plane-api
[READ ONLY MIRROR] Envoy REST/proto API definitions and documentation.
docx4j
JAXB-based Java library for Word docx, Powerpoint pptx, and Excel xlsx files
draft-irtf-cfrg-hpke
Hybrid Public Key Encryption
easycrypt
EasyCrypt: Computer-Aided Cryptographic Proofs
enchant
enchant spellchecking library
envoy
Cloud-native high-performance edge/middle/service proxy
equational_theories
A project to map out the relations between different equational theories of Magmas.
file
Read-only mirror of file CVS repository, updated every half hour. NOTE: do not make pull requests here, nor comment any commits, submit them usual way to bug tracker or to the mailing list. Maintainer(s) are not tracking this git mirror.
flex
The Fast Lexical Analyzer - scanner generator for lexing in C and C++
FLT
Ongoing Lean formalisation of the proof of Fermat's Last Theorem
formal-conjectures
A collection of formalized statements of conjectures in Lean.
formalising-mathematics
Lean 3 material for Kevin Buzzard's 2021 TCC courrse on formalising mathematics. Lean 4 version available here: https://github.com/ImperialCollegeLondon/formalising-mathematics-2024
FStar
A Proof-oriented Programming Language
GlimpseOfLean
An introduction to theorem proving in Lean for the impatient.
grub
https://git.savannah.gnu.org/git/grub.git
hacl-star
HACL*, a formally verified cryptographic library written in F*
hacspec
Please see https://github.com/hacspec/hax
hax
A Rust verification tool
hax
A Rust verification tool
import-graph
Tool to analyse the import structure of lean projects.
karamel
KaRaMeL is a tool for extracting low-level F* programs to readable C code
lean4
Lean 4 programming language and theorem prover
lean4-metaprogramming-book
No description
LeanSearchClient
Syntax for searching with natural language from Lean, using https://leansearch.net/ (may extend to other services)
lean-smt
Tactics for discharging Lean goals into SMT solvers.
libcrux
The formally verified crypto library for Rust
list
The Public Suffix List
lk
LK embedded kernel
mathlib4
The math library of Lean 4
mm0
Metamath Zero specification language
natural_number_game
Building the natural numbers in Lean 3. The original natural number game, now frozen. See README for Lean 4 information.
NNG4
Natural Number Game
nss
Network Security Services (NSS)
opencode
The open source coding agent.
opencode
The open source coding agent.
openssl
General purpose TLS and crypto library
pernosco-submit
Tool for submitting traces to Pernosco
physlib
A project to digitalise results from physics into Lean.
plausible
No description
PrimeNumberTheoremAnd
Blueprint for the PNT+ Project
ProofWidgets4
Helper toolkit for creating your own Lean 4 UserWidgets
quote4
Intuitive, type-safe expression quotations for Lean 4.
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 environment for semi-interactive development of machine-checked proofs.
rocq-of-ocaml
Formal verification for OCaml, with Rocq
rr
Record and Replay Framework
sandwich
Sandwich is a multi-platform, multi-language, open-source library that provides a simple unified API for developers to use (multiple) cryptographic libraries in their applications.
sanitizers
AddressSanitizer, ThreadSanitizer, MemorySanitizer
SciLean
Scientific computing in Lean 4
sf-skills
Salesforce's curated collection of agent skills for building applications. Optimized for Agentforce Vibes, compatible with all AI tools.
SipHash
High-speed secure pseudorandom function for short messages
ssprove
A foundational framework for modular cryptographic proofs in Coq
verso
Lean documentation authoring tool
verus
Verified Rust for low-level systems code
WebGoat
WebGoat is a deliberately insecure application
wpf
WPF is a .NET Core UI framework for building Windows desktop applications.