Semantics Done Quick

Target output

We will use AI agents to lift trusted formal semantics for Pkl (warm-up) and Zig comptime (main). Target venue: PLDI 2027.

Summary

Before we can formally verify real-world systems, we need semantic models of real languages. We have such models for C, Rust, and a few others, but there is a long tail of unformalised languages, and people keep inventing new ones. We want to build semantic models fast, with AI doing most of the work, and trust the results in high-stakes settings.

Building such models has historically taken expert teams years, in some cases more than a decade (λJS, Cerberus, others). This is much too slow. We want to compress it to days, and trust the results nonetheless.

This project will use AI agents to build Lean 4 semantics for Apple's Pkl (warm-up) and a fragment of Zig's comptime evaluator (main work). We ask three things: how well can AI agents build such a model, and at what cost? How rigorously can we validate the result for use in high-stakes settings? And can we use the model to build downstream PL tools (verifiers, compilers, synthesisers)? Outputs: a Lean toolkit, semantics for both languages with evidence of fidelity, and a worked tool built on top.

High-level background

Three lines of work are foundational for this project.

There is a long and noble tradition of building tested operational semantics for messy real-world languages: λJS for JavaScript (Guha, Saftoiu, Krishnamurthi, ECOOP 2010), 'Python: The Full Monty' (Politz et al., OOPSLA 2013, which reports ~72 person-months), KJS in the K framework (Park, Stefanescu, Roșu, PLDI 2015), and Cerberus for C (Memarian, Sewell, et al., PLDI 2016 onwards). Each of these took a dedicated expert team years, in some cases more than a decade. This is much too slow.

Krishnamurthi, Lerner, and Elberty's 'The Next 700 Semantics: A Research Challenge' (SNAPL 2019) names automated semantics elicitation as an explicit open problem and documents four pre-LLM attempts at automation, all unsuccessful. They close with an explicit open question: can a system exploit prose documentation to make the problem tractable?

Recent capability results suggest the answer might be yes. Epoch and METR's MirrorCode benchmark (April 2026) shows frontier agents reimplementing multi-thousand-line programs from black-box behaviour, including Apple's Pkl. Basis.ai's April 2026 experiment showed multi-agent Claude Code generating a monolithic Lean 4 operational model for JavaScript, validated against Test262. Nobody has yet built a trustworthy and principled model, or used it as a basis for other formal tools.

Detailed technical background

Two works directly drive the project. Krishnamurthi, Lerner, and Elberty's 'The Next 700 Semantics' (SNAPL 2019) supplies the architecture, and Guha, Saftoiu, and Krishnamurthi's λJS (ECOOP 2010) supplies the worked example.

The architecture is straightforward. A surface language P is the messy real-world artefact (e.g. Zig, JavaScript, Pkl). A core language λP is a small lambda-calculus-style essence; the canonical λJS has nine constructs, while richer languages like Python have produced larger cores in practice. A desugaring function maps surface programs into core programs. The core interpreter is easy to write because λP is small. Validation runs the surface program through the real reference implementation, runs the core program through the λP interpreter, and checks the outputs match. The loop iterates over a corpus until they always do.

"Desugaring" is loose terminology when source and target differ substantially: Politz et al. 2013 make this point explicitly, calling theirs "really a compiler to a slightly different language". For Zig comptime in particular, our desugaring is closer to staged compilation than pure syntactic rewriting, because the source has a phase distinction (compile-time vs runtime) that λZig must preserve.

This decomposition matters because it splits the task into two very unequal halves. λP design is the small, taste-driven, insight-producing half, which the 2019 paper argues a human should do. Desugaring synthesis is the large, structural, search-heavy half, which the 2019 paper argues a machine should do. The 2019 attempts at the machine half all failed; the recent capability results suggest current frontier multi-agent LLM systems can succeed at this kind of structured code-generation task.

λJS is the canonical worked example of the architecture. It is a 9-construct core into which surface JavaScript desugars, and the 2012 follow-up paper (Politz et al., DLS 2012) tested the desugaring against a substantial corpus of real JavaScript programs. λJS-style cores are the model for what a good lifted artefact looks like: small, readable, analysable, with a desugaring function that is a tree homomorphism almost everywhere.

Our project departs from the 2019 framing in two ways. First, we use AI to accelerate the entire pipeline, λP design, desugaring, the small-step semantics, not just the desugaring synthesis the 2019 paper tried to automate. Human expert attention is reserved for the hard design judgements where AI is unreliable. Second, we use Lean 4 rather than Coq/Rocq, because the Lean AI tooling is strong (Mathlib coverage, plus automated theorem provers for Lean such as Kimina, Goedel-Prover, and DeepSeek-Prover).

We also treat the resulting Lean semantics as a foundation for further work, not as an end in itself. As stretch goals: a verifier built over the semantics (using Lean's proof infrastructure to prove properties of specific programs in λP), or a translation-validation-style proof to an IR such as AIR (Zig's typed intermediate representation after comptime evaluation). The 2019 framing stops at 'tests pass'; we want the semantics to be useful as well as faithful.

Proposed methodology

We hypothesise that with the surface/core/desugaring decomposition described above, frontier multi-agent LLMs can produce a trustworthy Lean semantics for a previously unmodelled language fragment in days to weeks, and that proof-grade validation evidence is achievable on bounded fragments of that semantics.

We will use Apple's Pkl as a warm-up target, and then Zig as our main target. We chose Zig because it is exactly the kind of language PL formalisation has not yet caught up with. Zig sits around #39 in mainstream popularity but is growing fast, with serious commercial users (Bun, TigerBeetle, Ghostty) and hundreds of thousands of developers. Zig's comptime itself is a novel language feature with no existing formal treatment: it allows compile-time metaprogramming using full Zig at the type level.

In both cases, we will follow the Krishnamurthi, Lerner, and Elberty surface/core/desugaring architecture. For each language we want four Lean artefacts: (i) the surface language as an AST; (ii) a small core λP, in the λJS tradition; (iii) a desugaring function from surface to core; and (iv) a small-step semantics for λP. The semantics of the surface language is then "desugar, then evaluate in λP". We validate against the reference implementation by randomised differential testing on a fuzzed corpus of programs.

The main work will be on a fragment of Zig's comptime evaluator, covering basic types, control flow, function application, and simple type-level computation. Memory and allocator semantics, cross-module generics, and async are out of scope, deferred for follow-on work.

We envisage a lifting loop that works as follows:

1. Inputs: the reference implementation and the language documentation.
2. The AI agent proposes an initial λP, desugaring, and small-step semantics.
3. A differential testing harness runs surface programs through both the real reference and the (desugar + λP) pipeline, flagging discrepancies.
4. The agent iterates, fixing the desugaring, growing λP, or revising the semantics. The mentor and mentees intervene on the hard design calls: where the agent is making a poor structural choice for λP, papering over a real ambiguity, or missing something the architecture ought to expose.
5. The loop has converged when tests pass on a fuzzed corpus (seeded from each language's reference test suite, expanded by grammar-aware fuzzing, with a held-out fraction reserved as the trust signal).

For the cost claim, we will benchmark against the human-labour numbers from the literature: λJS at multiple person-years (Guha et al. 2010, Politz et al. 2012), 'Python: The Full Monty' at 72 person-months including MOOC contributors (Politz et al. 2013), KJS at multi-year effort (Park et al. 2015), Cerberus at more than a decade and counting. We aim to compress this to days, measured in mentor-plus-mentee person-hours and frontier-model API spend.

Four open questions sit at the heart of the project, each something we expect the work itself to answer:

1. How much of the four-artefact pipeline (surface AST, λP, desugaring, small-step semantics) can frontier multi-agent LLMs produce autonomously, and where do they need expert intervention? Recent results (MirrorCode, Basis.ai) suggest the structural code is in reach; the design half is the more uncertain part of the bet.
2. Is randomised differential testing on a fuzzed corpus sufficient to drive the loop to convergence at AI-driven scale?
3. Does the surface/core/desugaring architecture transfer to Zig comptime? Comptime's phase distinction and type-level computation are unusual compared to the languages the architecture has been validated on (JavaScript and Python).
4. Is the chosen comptime fragment of Zig bounded enough to be tractable in four months, and stable enough across recent versions to be a useful target?

Two stretch goals are within reach if the core lifting work goes faster than expected. The first is a verifier built over the semantics: use Lean's existing proof infrastructure to prove properties of specific Zig programs by reasoning in λZig. A concrete demo target is a comptime-generated ComptimeStringMap proven correct, or a TigerBeetle-style invariant. The second is a translation-validation-style proof to an IR such as AIR (Zig's typed IR after comptime evaluation). This requires also formalising the relevant fragment of AIR's semantics in Lean and then proving per-program agreement between the spec's λP output and the real compiler's AIR output. We will pick which to pursue based on team progress and interest after the core work is settled.

By the end of the fellowship, success means the toolkit is working, both Pkl and Zig comptime semantics have been lifted and validated by differential testing, and at least one stretch goal has been started on the Zig semantics.

Preliminary experiments

MirrorCode shows frontier agents reimplementing real programs from black-box behaviour, and includes Pkl among its featured targets, giving us a ready-made behavioural oracle for the warm-up. The Basis.ai work shows multi-agent systems can produce Lean semantics at scale.

I've been building a few similar things at github.com/septract: lean-c-semantics lifts Cerberus's Core IR into Lean 4, currently passing 98% on a 760-test C corpus; the saw-core-lean branch of saw-script is a SAW→Lean backend; ACL2Lean is an ACL2-to-Lean4 bridge; claudes-cycles-lean is a Lean 4 / Mathlib formalisation of a recent Knuth theorem co-built with Claude.

Theory of impact

AI is generating code at speed and scale that defies direct human review. Formal verification is one of the best tools we have at that scale, and AI is rapidly making proof itself cheap. The bottleneck is now specification: you cannot verify a system until you can specify it, and most of the languages, ABIs, and APIs real-world code uses have no formal specification at all. Building one for a real language has historically taken a small team years.

If our toolkit reduces that cost by an order of magnitude, with auditable artefacts engineers can inspect and challenge, formal verification becomes feasible for languages and interfaces previously out of reach. The work feeds my broader programme on scalable formal oversight at Oath Technologies. Direct beneficiaries include Zig users in safety-critical contexts (TigerBeetle, kernel modules, embedded systems), and any community shipping AI-generated code checked against an underspecified target. All artefacts are open-source.

Risks and mitigations

Zig is pre-1.0 and the language will move during the fellowship. We pin to a specific Zig version at project start, treat newer versions as future work, and scope the comptime fragment to features that have been stable across recent releases.

The deepest worry is the coverage of the differential oracle: behavioural validation only tests programs in the corpus, and programs outside it can diverge silently from the real compiler. We follow Krishnamurthi (2019)'s established methodology, differential testing on a fuzzed corpus, the same approach that produced credible semantics for JavaScript and Python. Using the semantics for downstream verification gives a second-order check: successful proofs on real programs are evidence the semantics is internally consistent.

The Pkl warm-up depends on MirrorCode's behavioural oracle remaining usable, and on Pkl's reference implementation (Java/Kotlin) being callable from a Lean-side differential testing harness. If either path stalls, we fall back to a smaller hand-curated Pkl test corpus and run the warm-up on that.

Spec lifting is defensive infrastructure: it helps prove programs correct against trustworthy specs. We don't see a meaningful offence/defence asymmetry.

Capacity

4-5 hours per week, sustained across the fellowship period (June through September 2026), barring unforeseen circumstances. Some travel during August 2026 (unavailable 10-16 August specifically), accommodated through asynchronous communication; Zig design work is front-loaded into July to keep the high-judgement phase out of the travel window.

Timeline