agda

Here are 5 public repositories matching this topic...

tytolabs / umst-formal

Formal verification and categorical semantics for the Unified Material-State Tensor (UMST) — Agda, Coq, Lean 4, Haskell QuickCheck

haskell coq proof-assistant category-theory thermodynamics agda lean materials-science formal-verification umst

Updated Sep 8, 2026
Lean

SNAPKITTYWEST / sovereign-entropy-theorem

Star

Hallucination elimination via discrete minimization. Lean 4, Agda, CUDA-Q.

entropy agda formal-verification lean4

Updated Sep 3, 2026
Lean

tytolabs / umst-formal-double-slit

Star

The universe charges rent for knowing. Each bit of which-path information exacts an irreversible thermodynamic toll — and the interference pattern pays the price. Formally verified across Lean 4, Coq, Agda & Haskell. Zero sorry. 486 theorems. No exits.

haskell physics information-theory coq quantum-mechanics thermodynamics agda lean formal-verification umst

Updated Sep 2, 2026
Lean

bwbush / plfl

Star

agda lean

Updated Nov 15, 2025
Lean

bmorphism / paraoptic

Star

Para(C) - Optic(C) - Para(Optic(C)) formalized in Lean 4.28, Agda 2.8 (--safe --without-K), Dafny 4.11. Adversarially audited twice; killed claims documented.

category-theory agda optics dafny formal-verification lean4 open-games

Updated Aug 10, 2026
Lean

Add this topic to your repo

To associate your repository with the agda topic, visit your repo's landing page and select "manage topics."

Learn more