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

- Thread: https://externals.io/message/132920
- Original archive: https://news-web.php.net/php.internals/132920
- Started by Brian Nguyen on 2026-10-25T08:30:17+00:00
- Messages: 1
- Reply by email to internals@lists.php.net
- More for agents: search with https://externals.io/search.md?q={query} · RFCs at https://externals.io/rfc.md · JSON API at https://externals.io/api · documentation at https://externals.io/llms.txt

---

## #132920 — Brian Nguyen — 2026-10-25T08:30:17+00:00

URL: https://externals.io/message/132920#132920

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.

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

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.

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