Kleene algebra, KAT, and relation algebra in Lean 4 / Mathlib, with completeness proofs and proof-producing tactics. Based on Damien Pous’s relation-algebra library.
-
Updated
Sep 19, 2026 - Lean
Kleene algebra, KAT, and relation algebra in Lean 4 / Mathlib, with completeness proofs and proof-producing tactics. Based on Damien Pous’s relation-algebra library.
The first formal security methodology designed for human-AI collaboration. Systematic. Evidence-based. Open source.
HybrautNav a three layer navigation stack consisting of Strategy, Tactical and Controller Layers.
Plutus Experimental Smart Contacts
To associate your repository with the formal-method topic, visit your repo's landing page and select "manage topics."