JsonSchema

A Lean 4 formalization of the JSON Schema semantics from Validation of Modern JSON Schema (Attouche, Baazizi, Colazzo, Ghelli, Sartiani, Scherzinger — POPL 2024, arXiv:2307.10034), with an executable validator proven correct against it.

import JsonSchema
open Lean (Json)

#eval do
  let schema ← JsonSchema.ofJson (json% {
    "type": "object",
    "required": ["name"],
    "properties": { "name": { "type": "string" },
                    "age":  { "type": "integer", "minimum": 0 } }
  })
  let ada := JVal.ofJson (json% { "name": "Ada", "age": 36 })
  let bad := JVal.ofJson (json% { "age": -1 })
  return (schema.validate ada, schema.validate bad)
-- Except.ok (true, false)   -- (`bad` is invalid: no "name", and age < 0)

json% is Lean's JSON-literal macro; JsonSchema.parse / JVal.parse take a String if you have raw text instead.

What it is

The paper's validation semantics are encoded as an inductive judgment (SJudg/KJudg/LJudg) . An executable validator is defined separately and proven correct with respect to that judgment: validate ⊨ SJudg, machine-checked, no sorry.

The specification covers the paper's semantics in full, including its metatheory (termination is the paper's Theorem 3). The paper's complexity results are out of scope.

The trust boundary

Following the paper, the validator assumes a schema is well-formed — every $ref resolves and there are no unguarded reference cycles (the paper's Definition 1). Under that assumption it is proven correct.

Everything before validation — parsing, resolving $id/$anchor/$ref, building the reference store — is the frontend. It is trusted, not proven; the paper likewise assumes this normalization done beforehand. The frontend and validator together are exercised end-to-end against the official JSON Schema Test Suite (draft 2020-12), which passes every core-feature test: 1275 / 1275.

Deviations from the RFCs

A few deliberate, documented departures:

• Regex. Pattern matching uses lean-regex — a formally verified engine — rather than a hand-rolled ECMA-262 implementation, so a handful of ECMA-specific edge cases differ.
• Formats. The format assertion is optional in the spec and off by default (active only under the format-assertion vocabulary). Recognizers for the common formats use a smaller, simpler semantics than the format RFCs: adequate to the test suite, not claimed equal to the RFCs. The per-format faithfulness tiers are documented in JsonSchema/Semantics/Validator/Terminals.lean.
• Number representation. Values use the JVal type, whose numbers are exact rationals (Rat) rather than the decimals Lean's own Json stores. Exact rationals make minimum/maximum/multipleOf total and exact, avoiding the floating-point errors that affect multipleOf in many validators. Rat is a superset of JSON's finite decimals (it can express 1/3, which no JSON number can), which shows only when printing back to JSON.

Using the project

git clone --recurse-submodules <repo>    # or clone plain and init the submodule at the suite step

The validate executable

validate checks one instance against one schema and prints the verdict:

lake exe validate schema.json instance.json    # → true / false

It preloads the draft-2020-12 metaschemas (from Metaschemas/) so a schema that references them resolves. Exit code is 0 for either verdict, and 2 on error (unreadable/unparsable input, or a keyword the formalization does not model — reported on stderr).

It's a thin wrapper for quick checks. A few things worth knowing about its scope:

• one schema and one instance per run, with a plain true/false verdict;
• references resolve against the preloaded metaschemas — nothing is fetched over the network;
• a keyword the formalization doesn't yet model is reported as an error.

For annotations, reusing a compiled schema across documents, or Lean.Json/JVal inputs, use the library API below.

As a library

The whole surface is two types — JsonSchema and JVal — and parse/validate:

JsonSchema.parse    : String    → Except String JsonSchema   -- compile a schema from text
JsonSchema.ofJson   : Lean.Json → Except String JsonSchema   -- … or from a Lean.Json (e.g. json%)
JVal.parse          : String    → Except String JVal         -- parse a JSON value
JsonSchema.validate : JsonSchema → JVal → Bool               -- the verdict

import JsonSchema

def validateText (schema doc : String) : Except String Bool := do
  let s ← JsonSchema.parse schema      -- compile the schema
  let v ← JVal.parse doc               -- parse the value
  return s.validate v

JsonSchema is a compiled schema — a parsed syntax tree plus a $ref table — that you build once and validate against; its internals are private, so a value can only come from a successful compile. JVal is a JSON value. parse/ofJson return Except (not Option), so a bad schema names the keyword it choked on. Worked examples are in JsonSchema/Examples/ — start with Quickstart (the API), then ModernKeywords, RecursiveSchema, ProvenCorrect.

The test suite

git submodule update --init    # fetch the pinned test-suite fixtures (skip if cloned with --recurse-submodules)
lake exe suite                 # build & run; exits non-zero on any failure or skip

lake exe suite runs the official JSON Schema Test Suite (draft 2020-12) through the verified validator and reports passed / failed / skipped. A keyword the formalization does not model is skipped and tallied by keyword — honest missing coverage — alongside a skip histogram. It also bootstraps the fixtures on first run. Pass a directory to run any suite-format tree, or --assert-format to also enforce format. Today: 1275 / 1275.

Layout

• JsonSchema/Syntax/ — the data model (JVal, SchemaAst, Store, Uri, Ref).
• JsonSchema/Semantics/Validator/ — the trusted spec: the SJudg judgment and its metatheory.
• JsonSchema/Validator/ — the proven implementation and its correctness proofs.
• JsonSchema/Frontend/ — the trusted pipeline: JSON → SchemaAst + reference store.
• JsonSchema/Examples/ — compile-checked usage demos.

Main.lean (the validate CLI) and Test/ (the conformance suite) are sister targets that depend on the library, not part of it.