-
cslib Public
Forked from leanprover/cslibThe Lean Computer Science Library (CSLib)
Lean Apache License 2.0 UpdatedJul 23, 2026 -
coinduction Public
Forked from damien-pous/coinductioncoinduction library for Coq
Rocq Prover GNU Lesser General Public License v3.0 UpdatedApr 23, 2026 -
-
-
pacing-types Public
A Rocq formalization of RTlola pacing annotations
Rocq Prover Creative Commons Attribution 4.0 International UpdatedFeb 24, 2026 -
SHDL Public
Forked from rafa-rrayes/SHDLA minimalist HDL built entirely from logic gates for education and experimentation. Compiles circuits to C so that they can run anywhere
Python GNU General Public License v3.0 UpdatedDec 11, 2025 -
aac-tactics Public
Forked from rocq-community/aac-tacticsCoq plugin providing tactics for rewriting universally quantified equations, modulo associative (and possibly commutative) operators [maintainer=@palmskog]
OCaml Other UpdatedJun 4, 2025 -
-
-
-
hyco-popl-2025 Public
Coq developpement accompanying the paper "Coinductive Proofs for Temporal Hyperliveness" to appear at POPL 2025
-
-
ocallm Public
Training a (tiny) language model in OCaml, from scratch
-
minilia Public
Minimalistic OCaml API to send LIA queries to Z3
-
InteractionTrees Public
Forked from DeepSpec/InteractionTreesA Library for Representing Recursive and Impure Programs in Coq
Coq MIT License UpdatedApr 19, 2024 -
pravda Public
Forked from livrelogique/pravdaPravda is a tool for teaching formal logic.
TypeScript GNU General Public License v2.0 UpdatedMar 14, 2024 -
-
-
-
-
minibug Public
Concise and documented COq formalization of a symbolic bug finder for IMP
Coq MIT License UpdatedJan 4, 2024 -
-
-
typst Public
Forked from typst/typstA new markup-based typesetting system that is powerful and easy to learn.
Rust Apache License 2.0 UpdatedMay 1, 2023 -
metamatix Public
A verified implementation of a metamath proof checker
-
color Public
Forked from fblanqui/colorCoq library on rewriting theory and termination
Coq Other UpdatedMar 15, 2023 -
verified-static-analyzer Public
A small & simple WIP verified static analyzer
-
catala Public
Forked from CatalaLang/catalaProgramming language for literate programming law specification
OCaml Apache License 2.0 UpdatedJan 15, 2023 -
mathlib Public
Forked from leanprover-community/mathlib3Lean mathematical components library
Lean Apache License 2.0 UpdatedDec 7, 2022 -
{{ message }}