Revera
GitHub
By the OneRegex initiative.

Regular expressions that give the same answer in every language.

Revera is a clean-room implementation of POSIX.1-2024 extended regular expressions. The engine is written once, checked against a formal model in Lean, and generated into native Go, Rust, Zig, C, C++ and TypeScript libraries. Same matches, same errors, same resource bounds, whatever the language.

Get started How it works
  • Machine-checked in Lean 4
  • Bounded memory and work
  • No bindings, no drift
main.go 
package main

import (
    "fmt"

    "github.com/oneregex/revera/go"
)

func main() {
    re := revera.MustNew(
        `[[:alpha:]]+@[[:alnum:].]+`,
        revera.NoCaptures(),
    )

    // What can one match cost on any input up to 64 KiB?
    c := re.Contract(65536)
    fmt.Println(c.HeapBytes(), c.StackBytes(), c.Steps())

    ok, _ := re.MatchString("write to alice@example.org")
    fmt.Println(ok)
}
Heap bound1158 bytes
Stack estimate4608 bytes

One engine source, printed into

  • Go
  • Rust
  • Zig
  • C
  • C++
  • TypeScript
  • Lean 4 model
The problem

Every regex library speaks its own dialect.

Regular expressions look universal. They are not. The same pattern can match different text, or fail differently, depending on which library runs it.

No two engines agree

Each implementation has its own features and quirks, and nothing guarantees that a pattern accepted by one returns the same result in another. Move a rule between two services written in different languages and its meaning can quietly change.

They sit in the security path

Regexes filter, validate and route untrusted input, and sometimes the pattern itself comes from a user. A mismatch is not a cosmetic bug. It is a bypass, a crash, or a server that stops answering.

There is no real specification

The closest thing is POSIX extended regular expressions, and POSIX.1-2024 brought them up to date with the features people expect. But no fully conforming implementation exists, apart from MinRX, which focuses on correctness and simplicity, not on performance or on other languages.

What Revera is

One engine, checked once, shipped to every language.

The OneRegex initiative builds precise, verified regex specifications that turn into trusted, interoperable libraries for any language. Revera is that idea applied to POSIX.1-2024 extended regular expressions.

A precise, executable specification

The ERE rules are written down twice: as a plain-language specification every engine implements, and as a formal Lean model the engine is checked against. Ambiguity has nowhere to hide.

The same answer everywhere

Every library comes from the same engine source and is cross-checked on the same corpus: the same matches, the same errors, the same resource reports. A rule that works in the Go service works identically in the Rust one.

Resource contracts

Before a match runs, a compiled pattern reports how much heap, stack and work it can cost on any input up to a chosen length. Provision for it, cap it, or reject the pattern before it ever touches a request.

Native, generated libraries

Go, Rust, Zig, C, C++ and TypeScript, each with a hand-written API in the shape that language expects on top of a generated engine. No bindings to a C library. A new language gets a correct, fast engine without a rewrite.

Resource contracts

Know the worst case before you run it.

Ask a compiled pattern what one match can cost on any input up to a chosen length. The answer is a bound, not a measurement of one run: it holds for every subject of that length or shorter. Size a service around it, reject a pattern that exceeds a budget, or refuse a request before doing any work.

  • Heap: the maximum number of bytes the match explicitly allocates.
  • Stack: an estimate of the deepest call stack, from fixed frame sizes shared by every target.
  • Steps: an upper bound on abstract work, counted as one step per loop iteration or function call.
  • Bounded even on failure: a search that would exceed the engine's memory capacity returns a capacity error instead of growing without limit.
// Pattern: [[:alpha:]]+@[[:alnum:].]+
// Compiled without captures. Inputs up to 65536 bytes.
c := re.Contract(65536)

c.HeapBytes()   1158        // bytes, whatever the input
c.StackBytes()  4608        // bytes, deepest call stack
c.Steps()       199953412   // abstract operations, at most

// Same pattern, same call, in every language:
// the six libraries report the same three numbers.

These are the actual figures the Go library reports for that pattern. Bounds are conservative on purpose. A pattern compiled with captures enabled is bounded by the general capture solver, and a deeply nested one can report a heap bound in the tens of gigabytes. That is the number you cannot rule out, which is exactly what you need to know before accepting the pattern.

How it works

Written once. Proved once. Printed into every language.

Revera is a pipeline, not six hand-written libraries. The engine is written in Vego, a strict subset of Go made for mechanical translation. A compiler exports it as an intermediate representation, and printers turn that one artifact into each target.

Vego source go/*.go A strict Go subset: no imports, no methods, no interfaces, no function values, no generics.
Vego IR revera.vego.json The release artifact. Every generated engine, and the Lean model, starts from this file.
Lean 4 well formed, checked, bounded Reads the exact shipped IR, proves it well formed, checks it against the ERE model.
Gothe source itself
Rustengine.rs
Zigengine.zig
Cengine.c
C++engine.cpp
TypeScriptengine.ts

The Lean development reads byte-for-byte copies of the shipped IR, so the artifact that is proved is the artifact the printers consume. Each target adds a small hand-written runtime and public API, and nothing else.

Idiomatic output

The same engine, native in your language.

Not bindings. Each library is the generated engine plus a small hand-written API in the shape that language expects.

package main

import (
    "fmt"
    "log"

    "github.com/oneregex/revera/go"
)

func main() {
    re, err := revera.New("(abc)([0-9]*)")
    if err != nil {
        log.Fatal(err)
    }
    groups, err := re.FindStringSubmatch("__abc12__")
    if err != nil {
        log.Fatal(err)
    }
    fmt.Println(groups[1])
}
use revera::Regex;

fn main() -> Result<(), revera::Error> {
    let re = Regex::new("(abc)([0-9]*)")?;
    let caps = re.captures("__abc12__")?.expect("a match");
    println!("{}", &caps[1]);
    Ok(())
}
const std = @import("std");
const revera = @import("revera");

pub fn main(init: std.process.Init) !void {
    var re = try revera.Regex.compile(init.gpa, "(abc)([0-9]*)", .{});
    defer re.deinit();

    var caps = (try re.captures("__abc12__")).?;
    defer caps.deinit();
    std.debug.print("{s}\n", .{caps.get(1).?.text()});
}
#include <stdio.h>
#include <revera/revera.h>

int main(void) {
    const char pattern[] = "(abc)([0-9]*)";
    const char subject[] = "__abc12__";
    revera_error error;
    revera_regex *re = revera_compile(pattern, sizeof(pattern) - 1, NULL, &error);
    if (re == NULL) {
        return 1;
    }

    revera_match groups[3];
    if (!revera_captures(re, subject, sizeof(subject) - 1, groups, 3, &error)) {
        revera_regex_free(re);
        return 1;
    }
    printf("%.*s\n", (int)(groups[1].end - groups[1].start),
           subject + groups[1].start);
    revera_regex_free(re);
}
#include <iostream>
#include <revera/revera.hpp>

int main() {
    revera::Regex re("(abc)([0-9]*)");
    auto caps = re.captures("__abc12__");
    if (!caps || !(*caps)[1]) {
        return 1;
    }
    std::cout << (*caps)[1]->str() << '\n';
}
import { Regex } from "@oneregex/revera";

const re = new Regex("(abc)([0-9]*)");
const caps = re.captures("__abc12__");
if (caps === null) {
    throw new Error("no match");
}
console.log(caps.get(1)?.text);
// every one of them prints: abc
Go
go get github.com/oneregex/revera/go
Rust
cargo add revera
Zig
zig fetch --save https://github.com/oneregex/revera/releases/download/v0.1.0/revera-zig-0.1.0.tar.gz
C and C++
find_package(Revera CONFIG REQUIRED) then link Revera::C or Revera::CXX
TypeScript
npm install @oneregex/revera
Correctness and interoperability

Tested across languages. Proved against the specification.

No single mechanism carries the claim. Each layer catches what the others cannot.

One corpus, every backend

The conformance kit runs the same fixed corpus of 86,704 commands, covering matches, errors, replacements, iteration and contract reports, through every generated backend, and compares each answer with the canonical Go engine. Random stress rounds, a fuzz seed pack and sanitizer builds are part of the same run.

A formal ERE model in Lean

The POSIX.1-2024 ERE rules are stated as a Lean definition, written from the standard text and not from any engine. The interpreted engine is checked against that definition on every constrained corpus case, and on an exhaustive sweep of 41,370 small patterns against every short subject, over 1.5 million executions.

Proofs about the shipped artifact

Lean decodes the exact IR files that ship, proves them well formed, and proves universal heap and step bounds for phase A of the matcher, along with the soundness of the meter that records those costs. The proved file is the released file.

The proofs have explicit limits, and the Lean README states each one. The corpus and exhaustive checks are finite, not universal. Non-POSIX locale behavior is outside the model. The link between the proved phase A properties and the shipped engine covers corpus executions that use phase A alone. The generated Rust, Zig, C, C++ and TypeScript engines are tied to the proved IR by the conformance corpus, not by a proof of the printers.

FAQ

Questions, answered.

Is this just another regex library?

No. Revera is a specification with a formal model, one engine source, and printers. You do not get a hand-ported library per language. You get engines generated from a single artifact that Lean checks against the ERE model, and that a shared corpus cross-checks against each other.

Which regular expression dialect is it?

POSIX.1-2024 extended regular expressions: leftmost-longest matching, bracket expressions with character classes, equivalence classes and collating elements, interval expressions, and the shortest-preferring repetition modifiers that the 2024 revision added. There are no backreferences and no Perl escapes, because the ERE language has none. If you need Perl-compatible syntax, the same approach is being worked on for PCRE.

What exactly is a resource contract?

For a compiled pattern and a maximum input length, Revera reports an upper bound on heap bytes, an upper bound on abstract work, and an estimate of stack use. The report applies to every subject up to that length. You can read it before running a match and use it to accept, reject or budget a pattern.

Does it use a C library under the hood?

No. Each library is the engine printed into that language, plus a small hand-written runtime and API. The C and C++ libraries are generated the same way as the others. The only shared data is the embedded locale tables.

What about locales and Unicode?

Patterns and subjects are UTF-8. Every library embeds the same generated tables, built from CLDR 48.2 and Unicode 17.0.0, for character classes, case mappings and collating data in 1,122 CLDR locales. A locale-aware pattern therefore behaves the same in every language. The default locale is POSIX, and the generator that reproduces the tables lives in the repository.

What is Vego?

A strict subset of Go built for mechanical translation: no imports, no methods, no interfaces, no function values, no generics. The engine is written in it, so the Go library runs the source directly while the compiler exports the same code as an intermediate representation for the other printers and for Lean. The checker rejects anything outside the subset and points at the line.

Is it vibe-coded AI slop?

Revera is heavily AI-assisted. But agents have very little freedom. Every change is constrained by a written, ahead-of-time design and specification, the POSIX standard text, a conformance corpus that every backend must reproduce, differential fuzzing, generated files that must match the checked-in ones byte for byte, Lean proofs that read the shipped artifact, and manual review. If an agent produces incorrect code or drifts from the design, those constraints are meant to catch it immediately. Multiple large models are also systematically used to review and challenge every change.

Give every language the same regex.

One behavior in every language: correct, interoperable, resource-aware POSIX regular expressions, generated from one verified source.

Star on GitHub Read the README