Sha'ar 驗證兩個 AI 生成的 PostgreSQL TLS 補丁：一個通過，另一個令 PostgreSQL 在 OpenSSL 3.0.22 下無法啟動

What happens when an AI coding agent proposes a change that works on a modern system but breaks compatibility with an older one?

That's the question behind Sha'ar by Masora, an experimental verification system developed for the Meta Global AI Developer Hackathon.

The idea is simple:

The agent proposes. A deterministic gate decides.

The experiment

The target was a real infrastructure problem: PostgreSQL's default TLS key-exchange groups.

The objective was to introduce hybrid post-quantum key exchange using X25519MLKEM768, while preserving classical compatibility where required.

Two Meta-powered models independently proposed patches:

Muse Spark, through Meta's hosted Model API.

Muse Spark Open, through Baseten.

Instead of accepting a patch because a model generated it or because it looked correct, Sha'ar subjected each proposal to independently defined verification criteria.

The result

One proposal passed. The other failed.

The hosted Muse Spark proposal satisfied all 21 mandatory checks.

The Muse Spark Open proposal was rejected after exposing a compatibility failure: PostgreSQL could not start successfully when built against OpenSSL 3.0.

That distinction matters.

A change can look reasonable, compile successfully in one environment, and still violate a requirement elsewhere.

For security-sensitive infrastructure, successful code generation is not sufficient evidence of correctness.

What the gate actually checks

Sha'ar's deterministic verification workflow includes:

Applying proposed patches against a pinned PostgreSQL source revision.

Building against OpenSSL 3.6.3 and 3.0.22.

Running the PostgreSQL regression suite, covering 239 tests.

Observing real TLS handshakes rather than trusting generated descriptions.

Evaluating 21 mandatory checks.

Recording hash-chained evidence that can be independently inspected and verified.

The acceptance decision is made by deterministic software, not by asking another language model whether the patch looks safe.

Both saved proposals were subsequently reverified under the corrected gate without making additional model calls.

Why this matters beyond TLS

AI coding agents are increasingly capable of proposing substantial changes.

But the question is not merely:

Can an agent generate a plausible patch?

It's:

Can we establish, using independently checkable evidence, that the proposed change satisfies the requirements we actually care about?

For this experiment, an older-library startup failure was enough to reject a proposal that might otherwise have appeared promising.

The broader engineering principle is to separate proposal generation from acceptance authority.

See the experiment

🎥 Watch the 2:50 demonstration:
https://x.com/dg_zoskales/status/2118145938330181748

Source code and verification evidence:
https://github.com/dguchie/shaar

Sha'ar is an experimental prototype, not a production-ready autonomous repair system or a general proof that AI-generated code is safe.

Its demonstrated result is specific: two model-generated proposals, explicit acceptance criteria, and independently inspectable outcomes.

A question for the community

If you were designing a deterministic gate for AI-generated infrastructure changes, what failure would you insist on testing before accepting a patch?

Backward compatibility? Dependency drift? Security invariants? Something harder to capture?

I'd be interested in the engineering community's perspective.

Disclosure: This article was prepared with AI writing assistance. The technical claims refer to the project's published verification evidence.