proof-engineering

BibTeX bibliographies for proof engineering-related papers

An exhaustive condensed detachment formal proof generator for Hilbert systems in proof theory.

A comprehensive, production-grade robot vacuum cleaner simulation system with dual Julia and Rust implementations, GraphQL API, SLAM algorithms, and enterprise CI/CD infrastructure.

REPLICA: REPL Instrumentation for Coq Analysis

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.

Universal chat extraction tool

Artifact for "Proof Repair across Quotient Type Equivalences" paper (OOPSLA 2025 paper)

Live proof playground for neurosymbolic theorem provers

Feature flag management with fire-and-forget semantics

Thunderbird email template management - reloaded

Research language whose affine/QTT core is proved sound twice — Coq and Idris2, axiom-free and CI-gated — with the verified usage-checker ported into the Rust compiler. Nested Solo ⊂ Duet ⊂ Ensemble dialects, session-typed concurrency, echo types for loss that isn't erasure. Early alpha.

Multi-prover formal verification of Certified Null Operations (CNO: programs provably computing nothing) and Observational Null Disclosure (OND: programs provably revealing nothing). Two co-equal, logically independent pillars verified across Coq, Lean 4, and Agda, with axiom counts and out-of-scope residue lists honestly surfaced.

Catches the bugs tests miss and the bogus proofs LLMs write. Source code → Lean 4 with five validation gates.

The Role of Thoughts: a Dynamic Cognitive Mixture-of-Experts router for Claude Code. 9 expert lenses, 10 routing lanes, an R/s+ divergence gauge -- specified in 1770 machine-checked Lean 4 theorems across 99 modules, with 797 mutants applied and 797 killed, and 84 checkers behind 83 release gates.

APM-installable agent skills for Lean 4 and Mathlib4 — proof tactics, math domains, review and research workflows, generic tooling.

Coq-JR — Coq proof toolchain

Continuity-preserving software transitions: a language research prototype with Agda and Lean proofs and an Elixir reference runner.

Work in progress: evidence-indexed residual types; checked minimal Agda core, Echo/Epistemic comparisons and a separate finite explorer.

A comprehensive Coq formalization of the Collatz conjecture with a combinatorial analysis framework. Proves linear division advantage.

Computational and mathematical research archive and proof-engineering workspace for experimental approaches to the Riemann Hypothesis, Li-Keiper positivity, and related spectral/arithmetic structures.