[Showcase] Legalis-RS: A Cross-Jurisdictional Legal Framework in Rust (v0.1.4)

announcements
1

Hi everyone,

I’m excited to announce the release and share Legalis-RS (v0.1.4), a project with a slightly insane ambition: Modeling the world's legal systems into a single, type-safe Rust framework.

We often talk about "Law as Code," but usually it's limited to a single domain or country. We decided to take the hard path. We are building an infrastructure that abstracts and unifies diverse legal systems—from Civil Law jurisdictions (Japan, Germany, France, Laos, South Korea) to Common Law jurisdictions (USA, UK, Singapore, India, South Africa).

The Challenge: "Type-Checking" the World

Legal systems are the ultimate "legacy codebases." They are contradictory, jurisdiction-dependent, and structurally chaotic.

  • Civil Law relies on structured Codes (e.g., Japanese Civil Code, BGB).
  • Common Law relies on Case Law and Statutes.
  • Regulations vary from GDPR (EU) to local ordinances.

Trying to fit these into a unified Rust type system is a massive architectural challenge. But that’s exactly why we chose Rust. We need Enums that can represent the diversity of global governance, Traits that abstract legal effects, and Zero-Cost Abstractions to handle millions of statutes without runtime overhead.

What’s in v0.1.4?

The project has grown significantly beyond its initial release. We now support parsing and structural analysis for:

  • :japan: Japan: Civil Code, Companies Act, e-Gov XML parsing.
  • :united_states: USA / :united_kingdom: UK / :singapore: Singapore: Common Law structures and statutes.
  • :european_union: EU: GDPR and supranational regulations.
  • :laos: Laos / :south_korea: Korea / :india: India / :south_africa: South Africa: Expanding our comparative law coverage (including ODA-influenced legal transplants).

Why this is exciting for Rustaceans: Law via SMT Solving

This isn't just a parser; it's a Computational Law Engine powered by OxiZ (Pure Rust re-implementation of Z3 Theorem Prover).

We are treating legal statutes not just as text, but as logical predicates. By integrating an SMT solver, we aim to:

  • Find Isomorphisms: Mathematically prove structural similarities between the "Lao Civil Code 2020" and its "Japanese Civil Code" origins.
  • Verify Consistency: Use formal verification techniques to detect logical contradictions ("bugs") within or across jurisdictions.
  • Solve Law: Treat legal constraints as solvable equations.

If you are interested in Formal Verification, Domain-Driven Design (DDD), or seeing how we handle the "undefined behavior" of human laws using a theorem prover, come take a look.

Get Involved

We are looking for contributors who are interested in specific jurisdictions or the core architecture of legal simulation.

Let's build the std::law for the world!

2 Likes
2

What in the world?

Not gonna lie, this sounds super intriguing -- but "We fused legal systems with the Rust type system" was not on my bingo card for 2026 .. or any future year, for that matter.

Major kudos for the creativity!

My new personal pet project is to make this fit in somehow:

pub enum LegalInterpretation {
  /// Typos are actionable.
  WordOfTheLaw,

  /// Typos are mere boo-boos.
  SpiritOfTheLaw
}
1 Like
3

I would never trust a machine to be able to actually do law. I would trust it to do basic math/logic though… So I’m wondering how well this SMT solver of yours works, so I tried it out for fun.

Why does it claim this example [slightly modified from an example I’ve found in your repo] to be satisfiable though !?

fn main() {
    use num_bigint::BigInt;
    use oxiz::{Solver, SolverResult, TermManager};

    let mut solver = Solver::new();
    solver.set_logic("LIA"); // Integer arithmetic
    let mut tm = TermManager::new();

    // Create variables
    let x = tm.mk_var("x", tm.sorts.int_sort);
    let y = tm.mk_var("y", tm.sorts.int_sort);

    // x + y = 10
    let sum = tm.mk_add([x, y]);
    let ten = tm.mk_int(BigInt::from(10));
    let eq = tm.mk_eq(sum, ten);

    // x > 5
    let five = tm.mk_int(BigInt::from(5));
    let gt = tm.mk_gt(x, five);
    // x < 6
    let six = tm.mk_int(BigInt::from(6));
    let lt = tm.mk_lt(x, six);

    // Assert and solve
    solver.assert(eq, &mut tm);
    solver.assert(gt, &mut tm);
    solver.assert(lt, &mut tm);

    match solver.check(&mut tm) {
        SolverResult::Sat => {
            println!("SAT");

            let m = solver.model().unwrap();
            println!("{}", m.pretty_print(&mut tm));
        }
        SolverResult::Unsat => println!("UNSAT"),
        SolverResult::Unknown => println!("Unknown"),
    }
}

output:

SAT
(model
  (define-fun Spur(2) () Int 5)
  (define-fun Spur(1) () Int 5)
)

How is it (apparently) failing at most basic arithmetic?

2 Likes
4

Great catch! This was a genuine bug in OxiZ's arithmetic solver.

Root cause: The LIA (Linear Integer Arithmetic) solver was using delta-rationals for strict inequalities, which works for reals but
not integers. For integers, x > 5 AND x < 6 has no solution since there's no integer in (5, 6).

Fix: Strict inequalities are now properly transformed for integer arithmetic:

  • x > k → x >= k + 1
  • x < k → x <= k - 1

This will be released in OxiZ 0.1.3. Thanks for helping improve the solver!

5

Wow.

Two things come to mind :

  • Once you encore civil code of most countries to rust enums, you would likely have million-variant enums. That would certainly stress-test the compiler !
  • You are making almost one new crate announcement a week, recently. How many are you in this organization and what kind of funding did you get? Objectives of the crates seem wildly different and creative.
6

They seem to be heavily LLM-oriented: their website, prose, and pictures are all AI-generated.

2 Likes
7

Thanks for the thoughtful questions!

  1. About “million-variant enums”
    Totally agreed — encoding every statute as a flat enum would be a compiler stress test and not a great representation anyway.
    Our approach is data-driven: the engine models the structure of a codebase (e.g., Part/Chapter/Article) as a small set of recursive types (an AST/IR),
    while the jurisdiction-specific content (and any annotations/metadata) lives as data payloads loaded at runtime (or via separate data crates).
    As the amount of jurisdiction data grows, we plan to keep the core engine lightweight and split jurisdiction datasets into separate crates/repos.

  2. About team size, velocity, and funding
    No VC here. This is currently mostly self-funded and maintained by a very small group (in practice: I drive architecture/specs and do reviews; contributions are welcome).
    For speed, I use LLM-assisted tooling for repetitive/boilerplate-heavy parts (tests, glue code, scaffolding), but changes are still human-reviewed and CI-tested.
    If you’re curious, we also just opened GitHub Sponsors — but either way, feedback like yours is already a big help.