Re: [RFC Idea] Formalization moratorium after PHP2Shell (CVE-2026-109618/109619): independent implementations in Rocq/Agda/K/Redex

On 10/25/26 03:30, Brian Nguyen wrote:

Hi internals, Summary: In October 2026 two critical runtime vulnerabilities, CVE-2026-109618 and CVE-2026-109619 (PHP2Shell, CVSS 9.2, fixed in 8.2.35 / 8.3.36 / 8.4.27 / 8.5.12 on Oct 21), were found in the Zend Memory Manager and HashTable / session upload progress handling. Not in ext/dom, ext/curl, or any application — in the allocator and stale request globals. This affects essentially every SAPI (FPM, mod_php, CGI, FrankenPHP). Motivation - mono-implementation brittleness: PHP is still defined by a single implementation. Efforts like php-langspec and KPHP were abandoned in the PHP 7 era. Today PHP_CodeSniffer, PHP-CS-Fixer, and PHP-Parser each maintain their own partial parsers, PeachPie must add workarounds for Laravel, and HHVM abandoned PHP compatibility in 2019 to become Hack. Without a second implementation and a formal spec, we have no way to catch this class of bug early. Cost of cosmetic deprecations: We have just deprecated non-canonical casts: (integer) -> (int), (boolean) -> (bool), (double) -> (float), (binary) -> (string). They are functionally identical. While well-intentioned for consistency, each such deprecation forces churn across tooling and user code. That time is not spent on reinforcing the base — exactly what PHP2Shell shows we need. Proposal: 1. Impose an immediate embargo on all new features and all cosmetic deprecations until the mono-implementation situation is rectified. Not adding a feature cannot break apps. Not deprecating (integer) cannot break apps. A corrupt allocator can.

You're asking the maintainers of Zend PHP to stop building Zend PHP and focus their efforts on building another implementation?

2. Complete the spec attempt left behind by 【entity-Facebook¦canonical_name=Facebook】 by reading php-src with AI assistance.

I agree that this spec should be kept up-to-date. Doing so requires 【entity-volunteers¦canonical_name=volunteers】.

3. Do not do the old ArtCraft-style clone-in-Rust-first approach. Since this class of bug was found with AI, and AI can now write directly in formalized languages, I propose we implement directly in formal frameworks:

    a) Extract and standardize the two ground truths: Zend Engine bytecode

and the formal parser.

    b) Build 4 independent implementations directly: two operational

semantics in K Semantic Framework and Racket PLT Redex, and two mechanized definitions in Rocq and Agda.

    c) Build a PyPy/Roslyn-style compiler from PHP to bytecode/JS from those

definitions to bootstrap semantics.

    d) Cross-test all implementations against php-src tests AND WordPress,

MediaWiki, Laravel, and other major codebases.

    e) Demonstrate bootstrapping by using the new implementations to compile

the bootstrapped runtime with itself. This gives us what other mature runtimes have: .NET has CoreCLR and still keeps a Mono option to stress-test additions; Python has PyPy, Cython, Brython. PHP needs the same.

The other implementations exist because the communities built them. The core developers of the reference implementations didn't decide to stop building their implementation to build the others. You're asking a group that's already stretched too thin with limited resources to stretch themselves further to build and maintain competing implementations. All of this is work that companies with the resources to build these implementations should be doing, contributing them back to the ecosystem to solve the problems that you've postulated.

I am not arguing for permanent stasis, only for sequencing: formalize and diversify first, then resume features. That is how we prevent irrelevance for greenfield projects. Thanks, Brian

Cheers, Ben