Hey There Buddo!

Monus, Factor, and Thinning Union Finds

Refinement Modeling and Verification of RISC-V Assembly using Knuckledragger

Thinnings: Sublist Witnesses and de Bruijn Index Shift Clumping

State of Knuckledragger III: Kernel Changes, Symbolic Union, AI, and more

An Associative-Commutative (AC) Hash Cons with AC matching

Weighted Union Find and Ground Knuth Bendix Completion

SMTLIB as a Compiler IR I

Calling Lean Functions As Python Functions

Term Ordering Etudes: Ground Lexicographic Path Ordering

Subterms Modulo Theories I

Contextual Union Finds

Dagstuhl Egraphs

Phil Wrapped 2025

SMTMSMT: Gluing Together CVC5 and Z3 Nelson Oppen Style

An Inequality Union Find Inspired by Atomic Asymmetric Completion

Our Latest Ouvres: The GCB and The Incident

Some Lean Syntax for Knuckledragger

Semi-Interactive Assembly Verification in Knuckledragger

SAT Etudes 2: Toy DPLL

Primitive, Leveled, and Quantifier Union Finds

Implementing E Unification using SMT

My House Mildly Burned Down

ZF style set theory in Knuckledragger I

Toy Binary Decision Diagrams

Proving the Infinitude of Primes in Knuckledragger

Proof Rules for MetaSMT

A Slotted Hash Cons for Alpha Invariance

Compositional Datalog on SQL: Relational Algebra of the Environment

A Python CLI for Verifying Assembly

Knuckledragger Analysis Etudes

Semantic Refinement/Dependent Typing for Knuckledragger/SMTLIB Pt 1

Verified Assembly 2: Memory, RISC-V, Cuts for Invariants, and Ghost Code

Semi-Automated Assembly Verification in Python using pypcode Semantics

Using Lean like an External SMT Solver from Python