BibTeX bibliographies for proof engineering-related papers
-
Updated
Jul 24, 2019 - TeX
#
proof-engineering
Here are 12 public repositories matching this topic...
REPLICA: REPL Instrumentation for Coq Analysis
analytics analysis repl coq replica user-study coq-plugin coq-ecosystem read-eval-print-loop user-study-tool proof-engineering
-
Updated
Jan 2, 2020 - Python
Lean Toolchain provides a collection of formally verified cryptographic algorithms, mathematical operations, and data parsing utilities. All implementations are proven correct in Lean 4 and can be extracted to high-performance Rust code.
rust dependent-types cryptography linear-algebra hmac sha256 formal-verification proof-engineering mathlib lean4
-
Updated
May 28, 2026 - Lean
Artifact for "Proof Repair across Quotient Type Equivalences" paper (OOPSLA 2025 paper)
-
Updated
Mar 3, 2024 - Agda
APM-installable agent skills for Lean 4 and Mathlib4 — proof tactics, math domains, review and research workflows, generic tooling.
-
Updated
Jun 13, 2026 - Python
A comprehensive Coq formalization of the Collatz conjecture with a combinatorial analysis framework. Proves linear division advantage.
coq theorem-proving formal-verification number-theory collatz-conjecture proof-engineering combinatorial-analysis hailstone-numbers kakutani-s-problem thwaites-conjecture syracuse-problem mathematical-proof mathematical-formalization
-
Updated
Mar 7, 2026 - Rocq Prover
A Formal Proof of the Irrationality of the Euler-Mascheroni Constant.
lean formal-verification number-theory irrational-numbers interactive-theorem-proving proof-engineering mathlib harmonic-series natural-logartihm computational-number-theory infinite-series euler-mascheroni proof-by-contradiction math-proof lean-prover constructive-proof sondow-identity
-
Updated
May 9, 2026 - Lean
Kernel-safe upper-compatible proof-engineering layer over Lean 4. spec def, concept, refines, obligations, proofplan, trust ledger.
theorem-proving proof-assistant lean formal-verification proof-engineering lean4 verified-software-engineering
-
Updated
Apr 29, 2026 - Lean
Solving software verification exercises using Athena
-
Updated
Sep 7, 2022
Catches the bugs tests miss and the bogus proofs LLMs write. Source code → Lean 4 with five validation gates.
-
Updated
May 7, 2026 - Python
Formal core of the Fulcrum governance kernel: Lean 4 proofs, claim ledger, and theorem inventory.
-
Updated
Jun 3, 2026 - Lean
Categorical Backend Experiment: QBE-derived compiler IR lab for semantic provenance and proof artifacts
-
Updated
May 13, 2026 - C
Improve this page
Add a description, image, and links to the proof-engineering topic page so that developers can more easily learn about it.
Add this topic to your repo
To associate your repository with the proof-engineering topic, visit your repo's landing page and select "manage topics."