KJS: A Complete Formal Semantics of JavaScript

JavaScript is one of the most widely used programming languages in the world, powering web browsers, server-side applications, and increasingly embedded systems. Despite its ubiquity, JavaScript had lacked a complete, formal, executable semantics -- a mathematically precise definition of how every program should behave. Park, Stefanescu, and Rosu present KJS, the most complete and thoroughly tested formal semantics of JavaScript to date, faithfully mechanizing the ECMAScript 5.1 standard in the K Framework. Being executable, KJS has been tested against the official ECMAScript conformance test suite (test262) and passes all 2,782 core language tests. Among all existing implementations of JavaScript, only Chrome V8 passes all these tests, and no other formal semantics of JavaScript passes more than 90%. This achievement demonstrates that it is possible to turn a complex, informal language standard into a rigorous formal artifact without sacrificing completeness or fidelity.

JavaScript's semantics is notoriously complex, featuring dynamic typing, prototypal inheritance, first-class functions with closures, implicit type coercions, a complex this binding mechanism, and numerous corner cases specified across 250+ pages of the ECMAScript standard. The standard itself is written in a semi-formal algorithmic pseudocode style that mixes specification-level constructs (like Completion records, Reference types, and Property Descriptors) with runtime behavior in ways that are difficult to formalize directly. Previous formalization efforts either covered significant subsets of the language (such as $\lambda_{JS}$ by Guha et al. and JSCert/JSRef by Bodin et al.) or adopted simplified models that deliberately omit complex features. KJS takes a different approach: rather than simplifying or re-interpreting the standard, it directly and faithfully encodes the standard's algorithmic specifications as K rewrite rules, preserving the standard's structure and intent while making it mathematically precise and executable.

The KJS semantics is developed in the K Framework, a rewriting-based semantic framework where language definitions consist of a configuration (defining the structure of the program state) and rewrite rules (defining computation steps). The KJS configuration contains cells for the computation stack (<k>), the execution context stack (tracking the running execution context, variable environments, lexical environments, and the this binding), environment records (declarative and object environments mapping identifiers to bindings), the object store (mapping object identifiers to their internal properties including [[Prototype]], [[Class]], [[Extensible]], [[Get]], [[Put]], [[Call]], [[Construct]], and named data/accessor properties), and global state cells. Each JavaScript object is represented as a map from property names to Property Descriptors (either data descriptors with [[Value]], [[Writable]], [[Enumerable]], [[Configurable]], or accessor descriptors with [[Get]], [[Set]]). The semantics uses a different namespace for internal semantic functions, prefixing them with @ to avoid polluting the global object:

rule <k> @GetValue(V:Reference) => @Get(V) ... </k>
     when isPropertyReference(V)
rule <k> @GetValue(V) => V ... </k>
     when notBool isReference(V)

A key design principle of KJS is its close correspondence to the ECMAScript standard. The standard defines numerous abstract operations and internal methods such as [[Get]], [[Put]], [[HasProperty]], [[DefaultValue]], [[DefineOwnProperty]], ToPrimitive, ToNumber, ToString, ToBoolean, ToObject, and the Abstract Equality Comparison Algorithm. Each of these is encoded as a K function or rewrite rule that mirrors the step-by-step algorithmic specification in the standard. For example, the Abstract Equality Comparison ($x == y$) involves a cascade of type checks and coercions: if the types match, strict comparison is used; if one operand is null and the other undefined, true is returned; if one is a number and the other a string, the string is converted via ToNumber; if either is a boolean, it is converted to a number; and if one is an object, ToPrimitive is invoked. This faithful encoding means that KJS inherits the standard's complexity but also its precision, capturing exactly the behaviors that conforming implementations must exhibit.

The handling of JavaScript's scope chain and closures requires careful modeling of Lexical Environments and Environment Records. Each function execution creates a new execution context with a new lexical environment, which contains an environment record (mapping variable names to values) and a reference to the outer lexical environment, forming the scope chain. The semantics distinguishes between declarative environment records (used for function scopes and block scopes) and object environment records (used for the with statement and the global scope). The arguments object, created for each non-strict function call, is particularly complex: it maintains live bindings to the function's formal parameters, meaning modifications to named properties of arguments are reflected in the corresponding parameter variables and vice versa. KJS models this with precision, including the differences between strict and non-strict mode behaviors, where strict mode disables the live binding and makes arguments behave as a regular object.

KJS passes all 2,782 core language tests in the ECMAScript 5.1 conformance test suite -- matching only Chrome V8 among all implementations and formal semantics.

Testing KJS against the conformance test suite revealed that the test suite itself was incomplete, failing to cover several semantic rules in the standard. The authors performed a semantic coverage analysis, systematically identifying which K rewrite rules in the semantics were not exercised by any test in the suite. They found exactly 17 semantic rules in the core semantics that were not covered by the test suite. For 11 of these uncovered behaviors, the authors were able to write test programs that exercised the missing rules. These new tests were then run against major production JavaScript engines -- Chrome V8, Safari WebKit (JavaScriptCore), and Firefox SpiderMonkey -- revealing previously unknown bugs in these production engines. The bugs included incorrect handling of edge cases in type conversion, property access on primitive values, and specific corner cases in the for-in statement. The authors also compared KJS against other formal semantics ($\lambda_{JS}$ and JSCert) and found that both contained errors that KJS's comprehensive testing methodology exposed.

Beyond concrete execution, KJS is symbolically executable, enabling formal analysis and verification of JavaScript programs. The K Framework's infrastructure provides a symbolic execution engine that can explore all possible execution paths through a program with symbolic inputs. Using this capability, the authors verified properties of non-trivial JavaScript programs, including demonstrating a known security vulnerability in a real-world code pattern. Symbolic execution with KJS allows reasoning about all possible runtime behaviors without needing to enumerate concrete test inputs, making it suitable for security analysis and program verification. The reachability logic prover built into K can take specifications (pre/post-condition pairs) and attempt to prove that a JavaScript program satisfies those specifications for all possible inputs, leveraging the complete semantics of KJS as the trusted computing base.

KJS compares favorably with prior JavaScript formalization efforts. The $\lambda_{JS}$ semantics by Guha, Saftoiu, and Krishnamurthi desugars JavaScript into a smaller core calculus, which simplifies reasoning but introduces a translation layer that can introduce discrepancies with the standard. JSCert/JSRef by Bodin, Chargueraud, Filaretti, Gardner, Maffeis, Naudziuniene, Schmitt, and Smith provides a Coq-mechanized semantics that more closely follows the standard, but at the time of publication passed only about 90% of the conformance tests. KJS's advantage is its combination of completeness (passing all core tests), direct correspondence with the standard (no desugaring or intermediate language), executability (functioning as an interpreter), and extensibility to symbolic execution (supporting verification). The K Framework's approach of deriving all tools from a single semantic definition ensures consistency between the interpreter and the verification tools.

The contributions of KJS extend beyond the immediate technical achievement. The work demonstrates that the K Framework's methodology -- defining a language's complete semantics once and automatically deriving interpreters, symbolic execution engines, and program verifiers -- scales to real-world, complex programming languages. JavaScript's semantic complexity, with its dynamic typing, prototypal inheritance, implicit coercions, and numerous corner cases, represents a significant stress test for any formalization framework. KJS's success establishes that formal semantics need not be restricted to idealized or subset languages but can faithfully capture the full complexity of production language standards. The semantics and all related artifacts are publicly available at https://github.com/kframework/javascript-semantics, serving as both a reference implementation and a foundation for future JavaScript analysis tools. The methodology pioneered by KJS has since been applied to other languages, including C (with the companion work on undefinedness by Hathhorn et al.) and the Ethereum Virtual Machine (KEVM), demonstrating the generality and scalability of the approach.