Revera

main.go

package main

import (
    "fmt"

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

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

    // What can one search 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)
}

Regex engines can disagree

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.

The standard still needs choices

POSIX extended regular expressions provide a real specification, updated in POSIX.1-2024. They also leave some behavior undefined, unspecified or implementation-defined. Revera documents those choices and applies them consistently in every generated engine.

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. The remaining implementation choices are documented explicitly.

Cross-checked 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. The suite compares each rule through every backend.

Resource contracts

Before a search runs, a compiled pattern reports portable heap and work bounds, plus a stack estimate, for 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 starts from the same checked IR instead of reimplementing regex semantics.

Resource contracts

Know the worst case before you run it.

// Pattern: [[:alpha:]]+@[[:alnum:].]+
// Compiled without captures. Inputs up to 65536 bytes.
c := re.Contract(65536)

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

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

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 versioned engine artifact. Every generated engine, and the Lean model, starts from this file.

Lean 4 well formed, checked, bounded Reads the exact IR, proves it well formed, and checks it against the ERE model within the documented scope.

Gothe source itself

Rustengine.rs

Zigengine.zig

Cengine.c

C++engine.cpp

TypeScriptengine.ts

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);

One corpus, every backend

The conformance kit runs the same fixed corpus of 90,145 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 checked-in IR consumed by the printers.