~1K LOC for parallel & sandboxed mutation testing (https://github.com/pkhuong/ppb/blob/main/mutants.py). I could probably do better with a real parsing library?
Paul Khuong
- 507 Followers
- 390 Following
- 2.2K Posts
LeanNew Lean use case: Veil, a multi-modal verification framework for distributed protocols.
Distributed protocols underpin critical infrastructure, yet no single verification technique is sufficient. Model checking finds bugs but can't prove correctness. SMT solvers provide push-button proofs but fail outside decidable fragments. Proof assistants handle anything but demand manual effort.
Veil integrates all three in a unified framework embedded in Lean. Write a model once, then apply concrete and symbolic model checking, SMT-based proofs, and interactive theorem proving from a single executable specification. Its semantic foundations (provided by Loom) guarantee that what the model checker executes and what the SMT solver reasons about are provably the same system. Proofs produced by external solvers are checked by Lean's kernel via Lean-SMT.
Developed by George Pîrlea, Vladimir Gladshtein, Elad Kinsbruner, Qiyuan Zhao, and Ilya Sergey at the National University of Singapore. Under active development.
See the use case page for more: https://lean-lang.org/use-cases/veil
arXiv cs.LO botGaloisSAT: Differentiable Boolean Satisfiability Solving via Finite Field Algebra
Curie Kim, Carsten Portner, Mingju Liu, Steve Dai, Haoxing Ren, Brucek Khailany, Alvaro Velasquez, Ismail Alkhouri, Cunxi Yu
https://arxiv.org/abs/2603.28796 https://arxiv.org/pdf/2603.28796 https://arxiv.org/html/2603.28796
arXiv:2603.28796v1 Announce Type: new
Abstract: Boolean satisfiability (SAT) problem, the first problem proven to be NP-complete, has become a fundamental challenge in computational complexity, with widespread applications in optimization and verification across many domains. Despite significant algorithmic advances over the past two decades, the performance of SAT solvers has improved at a limited pace. Notably, the 2025 competition winner shows only about a 2X improvement over the 2006 winner in SAT Competition performance after nearly 20 years of effort. This paper introduces GaloisSAT, a novel hybrid GPU-CPU SAT solver that integrates a differentiable SAT solving engine powered by modern machine learning infrastructure on GPUs, followed by a traditional CDCL-based SAT solving stage on CPUs. GaloisSAT is benchmarked against the latest versions of state-of-the-art solvers, Kissat and CaDiCaL, using the SAT Competition 2024 benchmark suite. Results demonstrate substantial improvements in the official SAT Competition metric PAR-2 (penalized average runtime with a timeout of 5,000 seconds and a penalty factor of 2). Specifically, GaloisSAT achieves an 8.41X speedup in the satisfiable category and a 1.29X speedup in the unsatisfiable category compared to the strongest baselines.
toXiv_bot_toot
GaloisSAT: Differentiable Boolean Satisfiability Solving via Finite Field Algebra
Boolean satisfiability (SAT) problem, the first problem proven to be NP-complete, has become a fundamental challenge in computational complexity, with widespread applications in optimization and verification across many domains. Despite significant algorithmic advances over the past two decades, the performance of SAT solvers has improved at a limited pace. Notably, the 2025 competition winner shows only about a 2X improvement over the 2006 winner in SAT Competition performance after nearly 20 years of effort. This paper introduces GaloisSAT, a novel hybrid GPU-CPU SAT solver that integrates a differentiable SAT solving engine powered by modern machine learning infrastructure on GPUs, followed by a traditional CDCL-based SAT solving stage on CPUs. GaloisSAT is benchmarked against the latest versions of state-of-the-art solvers, Kissat and CaDiCaL, using the SAT Competition 2024 benchmark suite. Results demonstrate substantial improvements in the official SAT Competition metric PAR-2 (penalized average runtime with a timeout of 5,000 seconds and a penalty factor of 2). Specifically, GaloisSAT achieves an 8.41X speedup in the satisfiable category and a 1.29X speedup in the unsatisfiable category compared to the strongest baselines.
DyalogIn our latest blog post – https://www.dyalog.com/blog/2026/04/dyalog-v20-4-1-automatic-tacification/ – Adám introduces an exciting and long-overdue enhancement that will automatically convert all your code into tacit form whenever it is saved
James Endres HowellUhhh, guys? This looks real bad
"GNU Emacs: Multiple Remote Code Execution Vectors on File Open"
https://github.com/califio/publications/blob/main/MADBugs/vim-vs-emacs-vs-claude/Emacs.md
That's just enough to implement https://github.com/pkhuong/ppb/blob/main/examples/picoscope.c, a stripped down version of https://github.com/protocolbuffers/protoscope's decoder
There's a bunch of simplistic JSON parsers. I felt the need to write something similar for protobuf, so here's https://github.com/pkhuong/ppb
The basic idea is you predeclare all the fields you're interested in (including catch-all fields, as an option), prescan to gather stats like number of occurrence and total number of bytes, for each field (just enough to preallocate), then lex the same bytes again to get individual field info, in order.
I find proof engineering with Frama-C's WP plugin can be pretty churny, but nearly all in annotations. Is there a good way to isolate proof-only changes from regular code change in version control?
arXiv math.LO botSpeedability of computably approximable reals and their approximations
George Barmpalias, Nan Fang, Wolfgang Merkle, Ivan Titov
https://arxiv.org/abs/2603.26484 https://arxiv.org/pdf/2603.26484 https://arxiv.org/html/2603.26484
arXiv:2603.26484v1 Announce Type: new
Abstract: An approximation of a real is a sequence of rational numbers that converges to the real. An approximation is left-c.e. if it is computable and nondecreasing and is d.c.e. if it is computable and has bounded variation. A real is computably approximable if it has some computable approximation, and left-c.e. and d.c.e. reals are defined accordingly.
An approximation $\{a_s\}_{s \in \omega}$ is speedable if there exists a nondecreasing computable function $f$ such that the approximation $\{a_{f(s)}\}_{s \in \omega}$ converges in a certain formal sense faster than $\{a_s\}_{s \in \omega}$. This leads to various notions of speedability for reals, e.g., one may require for a computably approximable real that either all or some of its approximations of a specific type are speedable.
Merkle and Titov established the equivalence of several speedability notions for left-c.e. reals that are defined in terms of left-c.e. approximations. We extend these results to d.c.e. reals and d.c.e. approximations, and we prove that in this setting, being speedable is equivalent to not being Martin-L\"{o}f random. Finally, we demonstrate that every computably approximable real has a computable approximation that is speedable.
toXiv_bot_toot
Speedability of computably approximable reals and their approximations
An approximation of a real is a sequence of rational numbers that converges to the real. An approximation is left-c.e. if it is computable and nondecreasing and is d.c.e. if it is computable and has bounded variation. A real is computably approximable if it has some computable approximation, and left-c.e. and d.c.e. reals are defined accordingly. An approximation $\{a_s\}_{s \in ω}$ is speedable if there exists a nondecreasing computable function $f$ such that the approximation $\{a_{f(s)}\}_{s \in ω}$ converges in a certain formal sense faster than $\{a_s\}_{s \in ω}$. This leads to various notions of speedability for reals, e.g., one may require for a computably approximable real that either all or some of its approximations of a specific type are speedable. Merkle and Titov established the equivalence of several speedability notions for left-c.e. reals that are defined in terms of left-c.e. approximations. We extend these results to d.c.e. reals and d.c.e. approximations, and we prove that in this setting, being speedable is equivalent to not being Martin-Löf random. Finally, we demonstrate that every computably approximable real has a computable approximation that is speedable.