一个直觉主义微型证明助手
个人项目 Knuckledragger，一个基于求解器的直觉主义交互式定理证明助手库，已开源在 GitHub。 
评论
点赞
收藏用字典实现有限代数效应
作者用 Python 字典实现有限代数效应，展示如何用简单数据结构建模副作用和计算上下文。文章通过具体代码示例说明代数效应的组合与处理机制，适合对编程语言理论和实践感兴趣的读者。
通过 Z3Py 让 TLA+ 与 x86 协同工作
作者尝试将 TLA+ 规范翻译为 Z3Py，以连接 Verus、CBMC 及汇编检查器，并探索交互式定理证明。这为形式化验证工程师提供了具体的工具链集成思路，特别是如何桥接高层规范与底层硬件验证。
提升项：让作用域清晰的语法更“笨”一点
Philip Zucker 提出将“作用域提升（lifting）”概念从 egraph 简化到基础项（term）层面，通过引入 Thinning 结构让作用域成为项的内生属性而非隐式上下文。文章展示了如何用 Python 实现带作用域信息的 Smart Constructor 和模式匹配，解决了变量捕获和替换时的作用域对齐问题。这种“去抽象化”的设计思路对构建形式化验证、编译器中间表示或符号计算引擎有直接参考价值，特别是处理高阶逻辑和依赖类型时的工程实践。
数组理论（ToA）并查集：支持破坏性存储的新数据结构
Philip Zucker 提出了一种将“数组理论”（Theory of Arrays）与并查集（Union Find）结合的新数据结构。通过在半持久化数据结构的 rerooting 技术上引入非可逆的边缘注解，实现了对破坏性存储（destructive store）的支持。文中提供了 Python 实现，展示了如何在并查集中维护映射关系，并讨论了其与 SMT 求解器中数组理论的关联及在扩展实数中的应用。这对构建高效的符号执行引擎或约束求解器有直接参考价值。
TD4 4位DIY CPU组装与编程完全指南
作者购买并组装了TD4这款4位DIY CPU套件。文章详细记录了焊接过程中的坑（如二极管方向、USB接口焊接顺序），深入解析了CPU内部原理（地址解码、指令集、寄存器、进位触发器等）。作者还分享了从简单LED闪烁到复杂上下计数程序的编写过程，并提供了自己写的Python汇编器和模拟器代码。最后提到了Nand2Tetris课程和Ben Eater项目作为延伸学习资源。这是一篇非常适合计算机组成原理爱好者和DIY硬件玩家的实战指南。
域、循环项与扁平方程系统
作者介绍了近期与Cheng Zhang等人关于将循环无限流式结构整合进e-graphs的讨论，并回顾了自己几年前在类似方向（coegraph）的工作。涉及前沿的图论与代数系统交叉研究，具有较强的一手交流性质。
提升 E-Graphs：一篇被 PLDI 2026 接收的论文
作者宣布其关于 Lifting E-Graphs 的论文被 PLDI 2026 的 EGRAPHS Workshop 接收。这是一个重要的学术认可信号，E-Graphs 是当前编译器和程序分析领域的热点话题，具有较高关注度。
从 eprover 读取证明对象与重写系统至 Knuckledragger
讲述如何将自动化推理工具 eprover 生成的证明对象和重写系统集成到 Knuckledragger 中。属于自动化定理证明领域的工程实现细节，适合对该领域感兴趣的开发者。
面向家庭的Python FrozenSet依赖类型理论
作者表达了将抽象事物“有限化”并放入日常框架（如Python的Frozenset）中处理依赖类型理论的尝试。这是一种将高阶类型理论与具体编程语言特性结合的个人实验性观点。
使用 Dump Calculus 进行函数的提升与降低
作者探讨如何构建无名 De Bruijn e-graph，并由此引出用于函数提升和降低的组合子设计。这是一篇涉及底层编译器理论、图重写系统和函数式编程组合子的深度技术思考，适合对形式化方法和 e-graphs 感兴趣的工程师。
为 Alpha 等价性简化/提升 E-图：第一阶段检查点
作者正在构建支持 Alpha 等价性的 e-graph（E-图）。在实现过程中，发现原本以为复杂度会失控，但随着理解加深，代码反而变得更简洁。本文是该项目的阶段性检查点记录，分享了从复杂到简化的认知过程。
带 Thinnings 的 Alpha 等价哈希共享
探讨在 egraph 技术中引入 thinnings 以实现 Alpha 等价哈希共享的技术步骤。这是编译器优化和符号计算领域的一个具体算法改进点。
Monus、Factor与稀疏并查集发现
作者分享了一种思考广义e-graphs或模理论的“食谱”，核心思路是将常规的并查集（Union Find）替换为某种广义的并查集概念。这是关于底层数据结构与等价关系建模的工程/理论探索。
使用 Knuckledragger 对 RISC-V 汇编进行细化建模与验证
介绍使用 Knuckledragger 工具对 RISC-V 汇编进行细化建模和验证的方法。Binary verification 在底层系统开发中有实际用途，涉及具体的形式化验证技术路径。
Thinnings：子列表见证与 de Bruijn 索引移位聚类
作者受 Mastodon 上 Conor McBride 关于 Thinnings 的讨论启发，认为这是首次见到去除了复杂理论包装的直观解释。这一概念帮助作者理清了思路，并激发了关于 Lambda Egraphs 和广义并查集的大量新想法，计划后续深入展开。
把 SMTLIB 当作编译器中间表示(IR)：SSA 即函数式编程的工程实践
作者提出利用 Z3 SMT 求解器的 AST 直接作为编译器中间表示(IR)。核心观点是 SSA 形式与函数式编程高度同构，通过将控制流图(CFG)的每个块映射为递归定义的函数，并利用 SMT 的 substitute_funs 进行展开和简化，从而在逻辑层面实现编译优化和验证。文章展示了从 Python 代码到 SMT 定义再到类汇编 IR 打印的完整转换过程，并探讨了将其应用于 QBE 解析和二进制分析的可能性。这是一种利用定理证明器特性来简化编译器前端设计的工程实践。
在 Python 中直接调用 Lean 函数：一种实用的混合编程实践
作者开发了一个名为 leancall 的 Python 库，旨在降低 Lean 编程语言与 Python 互操作的门槛。该工具通过序列化、解析器和 FFI 机制，让开发者能在 Python 中直接调用 Lean 函数。文章展示了两个具体案例：一是利用 Lean 编写控制器来控制强化学习环境中的 CartPole 平衡问题；二是使用 Lean 实现光线追踪算法并生成图像。作者指出，虽然 Lean 的数学库（Mathlib）很强，但其通用生态系统尚不完善，通过 Python 作为“胶水层”来利用其丰富的库资源是一种务实且高效的工作流。此外，文章还对比了性能开销，并探讨了直接内存访问等优化可能性。
SMTMSMT：用Nelson-Oppen风格将CVC5与Z3粘合在一起
作者通过Python代码演示了如何手动实现Nelson-Oppen算法，将Z3和CVC5两个独立的SMT求解器“粘合”在一起协同工作。文章不仅展示了理论上的纯化与传播步骤，还深入探讨了不同求解器间模型合并的难点及凸性假设的重要性。对于关注形式化验证、自动定理证明底层架构以及SMT求解器内部机制的技术读者来说，这是一篇极具实操价值和深度的工程解析。
用于Alpha不变性的槽位哈希共识技术解析
作者深入探讨了在e-graph和哈希共识中处理变量名无关性（Alpha Invariance）的技术难题。文章指出传统的规范化方法缺乏组合性，导致构建新项时需重新遍历。作者提出了一种“槽位哈希共识”（Slotted Hash Cons）方案，通过在节点间保留排列信息的惰性求值机制，实现了高效的变量标准化。文中包含大量Python代码示例，详细演示了从变量映射到结构规范化的实现过程，并延伸至联合查找结构和张量规范化的相关讨论。这是一篇面向编译器、形式化验证及自动推理领域的深度工程实践文章。
组合式 Datalog 与 SQL：基于环境关系代数的新视角
作者提出了一种将 Datalog 编译为 SQL 的新方法。核心观点是：SQL 的关系代数（Join）与 Datalog 解释器中的“环境绑定”（Environment）概念高度契合。通过将 Datalog 变量绑定视为关系连接，可以直接生成高效的 SQL 查询。文章还展示了一个有趣的技巧：利用对偶数（Dual Numbers）模拟自动微分，实现 Datalog 的半朴素（Semi-naive）固定点迭代优化，从而加速递归查询。包含 Python 实现和 Colab 示例。