Free & open source · verified in Lean

Regular expressions you can actually trust.

PCRE‑Vera is a formally verified implementation and specification of the PCRE regular‑expression language. It proves its matching semantics in Lean, computes a resource contract for every pattern, and builds an engine for your programming language (JavaScript, Go, ...): no C bindings, no drift.

Get started See it in action

Mechanically proved
Bounded time & memory
libpcre2‑compatible

main.go

package main

import pcrevera "github.com/PCRE-Vera/pcre-vera/gen/go"

func main() {
    re, _ := pcrevera.Compile(`(?<user>\w+)@(?<host>[\w.]+)`, pcrevera.Options{})

    // Ask, before running: what can this pattern cost?
    b := re.Bounds()
    fmt.Println(b.Cost, b.Stack, b.Memory)

    ovector, _ := re.Match(subject, 0, 0, pcrevera.DefaultLimits())
}

cost boundO(n) · proved

stackconstant

Built on a single mechanized specification

Lean 4 Go JavaScript libpcre2 oracle Differential fuzzing

The problem

PCRE is everywhere, and it's a liability.

Perl‑Compatible Regular Expressions are a building block of countless applications. But the way we get them into our programs hasn't kept up with how critical they've become.

One implementation, in C

There is effectively a single source of truth: libpcre2, a large C codebase. Every correct behavior lives behind that one artifact and its build configuration.

Bindings or half-measures

In other languages the choice is stark: wrap the C library, or rely on partial reimplementations that make no interoperability guarantees. Either way, behavior drifts.

A critical, unbounded component

A regex engine must be bug‑free, since flaws become security issues, and its CPU and memory use must stay under control when processing untrusted data. Today, neither is guaranteed.

What PCRE‑Vera is

One specification. Proved once. Run anywhere.

A formally verified implementation and specification of PCRE, designed from the start to be a trustworthy source for implementations in many languages.

A precise reference semantics

A specification of PCRE that is compatible with libpcre and precise enough to serve as the source for implementations in other programming languages: not an informal description, an executable one.

Resource contracts

For a given regular expression, PCRE‑Vera computes conservative upper bounds on the time and memory required to evaluate it, before you ever run a match.

Mechanically verified in Lean

The matching semantics and the contract analysis are verified in Lean, including proofs that the computed contracts are correct, not just plausible.

Generated, idiomatic targets

Code generators translate the verified specification into efficient, idiomatic Go and JavaScript. Additional target languages can be added using the same approach.

Resource contracts

Know the worst case before you run it.

A compiled pattern can tell you its worst‑case cost, stack depth, and scratch memory up front. Every match then runs under explicit hard limits and returns a deterministic ResourceExceeded instead of running long: never a blown host stack, never unbounded work.

Cost: a closed‑form upper bound on work, as a function of subject length.
Stack: an engine‑managed explicit stack with checked capacity; the host call stack stays constant.
Memory: a bound on every per‑call allocation, enabling allocation‑free matching with a preallocated context.
Classification: the pattern reports its complexity class; the linear case is proved sound.

$ pcre-vera analyze '(?<user>\w+)@(?<host>[\w.]+)'

# resource contract (conservative upper bounds)
cost    = 41·n + 12       # instruction visits, n = |subject|
stack   = 3·n + 8         # explicit backtrack entries
memory  = 512 B           # scratch, fixed for this pattern
class   = linear          # proved sound

$ match --limit cost=1000000 --limit memory=65536
OK  ovector=[0, 17, 0, 5, 6, 17]

How it works

Authored once. Proved once. Built for every language.

PCRE‑Vera is a pipeline, not a hand‑written library per language. The engine is written once in a small verified‑friendly intermediate representation; the same artifact is both proved in Lean and built for each target.

PCRE pattern (?<user>\w+)@...

Verified IR (TIR) parser + compiler + matcher

Lean 4 semantics ∧ contracts, proved

Code generators idiomatic Go · JavaScript

The artifact the proofs were checked against is the same artifact the generators consume, hash‑pinned, so the two can never drift apart.

Idiomatic output

The same engine, native in your language.

Not bindings. Pure Go and pure JavaScript, generated from the verified specification.

package main

import (
    "fmt"
    "log"

    pcrevera "github.com/PCRE-Vera/pcre-vera/gen/go"
)

func main() {
    re, err := pcrevera.Compile(`(?<user>\w+)@(?<host>[\w.]+)`, pcrevera.Options{})
    if err != nil {
        log.Fatal(err)
    }

    subject := []byte("write to alice@example.org, please")
    ovector, err := re.Match(subject, 0, 0, pcrevera.DefaultLimits())
    if err != nil {
        log.Fatal(err)
    }
    if ovector == nil {
        fmt.Println("no match")
        return
    }

    group := func(n int) string {
        return string(subject[ovector[2*n]:ovector[2*n+1]])
    }
    fmt.Printf("%s is %s at %s\n",
        group(0), group(re.SubexpIndex("user")), group(re.SubexpIndex("host")))
}

import { compile, defaultLimits } from "pcre-vera";

const re = compile(String.raw`(?<user>\w+)@(?<host>[\w.]+)`);

const subject = new TextEncoder().encode("write to alice@example.org, please");
const ovector = re.match(subject, { limits: defaultLimits() });

if (ovector === null) {
  console.log("no match");
} else {
  const group = (n) =>
    new TextDecoder().decode(subject.subarray(ovector[2 * n], ovector[2 * n + 1]));
  console.log(`${group(0)} is ${group(re.groupIndex("user"))} at ${group(re.groupIndex("host"))}`);
}

// both print: alice@example.org is alice at example.org

Correctness & interoperability

Tested against the reference. Proved against the spec.

Verification isn't a single proof; it's layered, so every claim has a mechanism behind it.

A pinned oracle

"Correct PCRE" isn't one behavior; it's one build. PCRE‑Vera pins a specific pcre2 release, its tarball hash, and its full configuration, so the ground truth is reproducible.

Differential testing & fuzzing

An extensive interoperability suite and fuzzing tools compare every generated engine against the pinned oracle and each other: match outcomes, capture offsets, and compile errors, edge cases included.

Lean proofs

The matching semantics and the contract analysis are mechanically verified in Lean, including that the computed resource contracts are correct. The proved artifact is the shipped artifact.

FAQ

Questions, answered.

Is this just another regex library?

No. PCRE‑Vera is a verified specification plus generators. You don't get a hand‑ported library per language; you get engines generated from a single artifact that was proved correct in Lean and checked against a pinned libpcre2.

Does it use the C library under the hood?

No. The Go and JavaScript outputs are pure, dependency‑free implementations in the target language, not bindings to libpcre2. The C library is only used as a test oracle.

What exactly is a "resource contract"?

For a given pattern, PCRE‑Vera computes conservative upper bounds on the time and memory needed to evaluate it, as a function of the subject length. You can read those bounds before running a match, and enforce them at match time as hard limits.

Does this make my app hard-realtime?

No. PCRE‑Vera guarantees deterministically bounded work per call and allocation‑free matching with a preallocated context. Garbage collection, JIT warmup, and scheduling belong to your runtime and sit outside the model.

Which languages are supported?

Go and JavaScript today, generated from the verified specification. Additional targets can be added using the same approach; the IR and proofs don't change.

Is it vibe-coded AI slop?

PCRE‑Vera is heavily AI‑assisted. But agents have little freedom; every step is constrained by a frozen, ahead‑of‑time design, a libpcre2 oracle, extensive mechanical tests, Lean proofs, generated conformance suites, and manual review. If an agent produces incorrect code or drifts from the design, the constraints are meant to catch it immediately. Multiple large models are also systematically used to review and challenge every change.

Is it free and open source?

Yes. PCRE‑Vera is a free, open‑source tool. It is the new name of the project formerly known as pcre-truste.

Bring provable PCRE to your stack.

High‑quality, interoperable, resource‑aware PCRE, for more programming languages.

Star on GitHub Read the docs