rulec
Write rules. Prove them. Compile them.
A little language for business rules — a shipping tariff, a coupon policy, an eligibility test, a tax table with its reduced rates and provisos. Conditions are written as tables, and around them go calculations, exceptions that take precedence over a main rule, provisos, a rule applied to another case, lists whose length is not fixed, and one step of a process whose state the caller keeps.
Little on purpose. There is no recursion and no state, and a cell looks at its own column and nothing else. That is what lets rulec prove that every input in the declared domain gets exactly one answer — shown over all of them, not sampled by tests. Only a rule that passes compiles, into ordinary functions in twelve languages with no runtime and no dependencies.
An agent can do the writing. What it hands back is a rule a person can read, not code. What fails the checks comes back with the input that causes it, and what only a person can decide comes back as a question.
What rulec does
Built on tables, so it can be proved
Conditions are written in tables, and a cell tests the value in its own column and nothing else. So each row is one box in the space of inputs, and whether the boxes leave a gap or overlap can be computed exactly. The same table is the specification a person reads and checks, and in the generated code each row is one branch. This one is the table in the picture above, and it is a row short.
Gaps and overlaps fail before anything runs
Not sampled: the whole declared range is walked. The missing row comes back as the input that falls through it, so the fix is one row, and what the fee is, only a person can say.
error[E104]: An unrounded value reaches the output
--> parcel.rule:19
|
19 | fee : money[USD, incl_tax]
| ^^^^^^^^^^^^^^^^^^^^ no rounding is declared
|
Example: some input computes to 35.5USD. down(1USD) gives 35USD,
half_up(1USD) gives 36USD and up(10USD) gives 40USD, so the rounding
mode moves the result by up to 5USD.
error[E103]: This column is length[in], but `22lb` is written here
--> parcel.rule:26 table size_of
|
26 | | <=22lb | envelope |
| ^^^^^^
|
`22lb` is not a unit of length[in].
Units and tax flags are types. Rounding has to be declared
A value carries its unit, and an amount its currency and whether tax is included, so dollars and grams will not add and a tax-inclusive amount will not pass for a tax-exclusive one. Every intermediate is shown to fit in int64. A numeric output has to say how its fractions settle, and the question comes with the money the choice moves: nothing is rounded silently.
table size_of
policy first
| girth | -> size : size_class |
| <=22in | envelope |
| <=60in | small |
| - | large |
table base_rate
policy unique
| dest | size | weight | -> base : money[USD, incl_tax] |
| north_america | envelope | - | 6USD |
| north_america | small | <=160oz | 12USD |
| north_america | small | >160oz | 18USD |
…
Tables stack
Because a cell sees only its own column, tables stack as deep as you like. Here one table decides the size class from the girth, and the next reads that class as a column of its own to price the parcel. Every table in the stack is checked the same way, a row that names a value the table above never produces is reported as one nothing reaches, and the answer comes back with the row that decided it in each table.
Exceptions and provisos are checked with the main rule
A rule is rarely one table. GOV.UK gives a minimum wage for each age band, then states the apprentice rate as an exception to it, so the exception is a table of its own that overrides the first. A proviso that reads as a sentence is a clause, and a calculation gets a name with define. The checks read the main rule and its exceptions as one: every input still has to land somewhere, and where two could apply, overrides has to say which wins, or the check fails.
machine order over step
carry state -> next_state
held amount_paid
initial received
final delivered, cancelled
never shipped after cancelled
once refund >0JPY
error[E126]: A sequence of calls reaches shipped after cancelled
--> order_lifecycle.rule:37 machine order
|
37 | never shipped after cancelled
| ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
|
Calls (from received):
1. at received, event = cancel, amount_paid = 0JPY → cancelled (table step row 2)
2. at cancelled, event = pay, amount_paid = 0JPY → paid (table step row 10)
3. at paid, event = ship, amount_paid = 0JPY → shipped (table step row 4)
State machines too, checked over every sequence of calls
An order is paid, shipped and delivered, or cancelled. A rule that is one step of such a process is an ordinary table of state and event, and a machine section saying which output comes back as the next call's state, where a case starts and ends, and what must never happen — here, that a cancelled order is shipped. The generated function still keeps nothing: the caller keeps the state. rulec check walks every sequence of calls a case can make, and a claim that breaks comes back as the shortest sequence that breaks it — here, a payment that arrives after the cancellation and puts the order back, which no single row of the table shows.
$ rulec certificate fee.rule > cert.json
$ proofs/.lake/build/bin/rulec-recheck --rule fee.rule cert.json
Fee (0.22.1), re-checked against the Lean proofs
FeeTable: 6 rows — complete, 6 rows reached, no two rows meet, 1 axes tiled
12 boxes read back from the cells they were written as
the digest is fee.rule's, and 12 cells are read back out of it
OK: every claim this program states was proved, by the theorems of RulecCert.
$ rulec test generated/ --proofs
…
ok fee (Rust, proof) 2 harnesses
The proofs are checked again, outside rulec
rulec certificate prints what the proofs rest on, and two programs that share no code with rulec check it again: one dependency-free Python file, and a checker built from a Lean 4 development in which it is a theorem that passing its checks makes the claims true. The generated Rust goes to the model checker Kani, which shows over every input in the declared domain that no table falls through and nothing overflows.
source gov = file "sources/uk-sdlt.md" sha256:799106ea8a821a00 # GOV.UK, Open Government Licence v3.0
table1 sha256:360409a5675d3552
table2 sha256:15d4ed0baca64189
table standard
policy unique
| price | -> band : rate[step 1%] |
| <=125000GBP | 0% |
| >125000GBP <=250000GBP | 2% | @gov table1
| >250000GBP <=925000GBP | 5% | @gov table1
| >925000GBP <=1500000GBP | 10% | @gov table1
| >1500000GBP | 12% | @gov table1
Cite the source, and pin the copy
Declare the document a rule was transcribed from with source, and cite the table each row came from — @gov table1, here GOV.UK's stamp duty rates. rulec source fetch keeps a copy beside the rule, and rulec source pin fixes it by its hash. From then on the rows are held to that copy: one wrong digit fails, and a figure the copy states that no row uses is W120, the other half of the same slip. A statute is cited by its section and pinned to the government's own text, on e-Gov or the eCFR, and an amendment names the rows to reread.
There is a page for people
rulec doc --format html renders the rule as one page a reader tries a case on: type a case, and the rows that matched light up and the answer appears. It is the generated JavaScript itself that runs, so the page says nothing the code does not. The document for people, with the cited copy set beside the rule's own table, and the article a help centre publishes come from the same rule.
Twelve languages, not a dependency between them
Python, TypeScript, JavaScript, Rust, Ruby, PHP, Go, Swift, Java, SQL, Wasm, and NumPy for whole columns at once. One row, one branch, with no runtime and no configuration. Beside each function, a _traced twin returns which row of which table decided the answer, which is what a log line or a reply to a customer needs.
Twelve targets · 112 diagnostics · 87 rules checked, generated and run on every commit — 34 transcribed from a published source · no dependencies, no runtime · one binary · the checks are offline
Where to start, by what you have
None of the three changes anything that runs today.
| you have | the first move | the command |
|---|---|---|
| a spreadsheet, a published policy or a statute | Transcribe it into a .rule and check it. A workbook gives a first draft straight out of the file, with every guess marked. A statute or a document is cited and kept as a copy. No data and no old implementation are needed |
rulec import xlsx, then rulec check — What it proves |
| an implementation that runs today | Transcribe it into a .rule and wrap the old code in a short adapter. verify runs the cases built from the rule's own boundaries through both, and returns where they disagree, clustered by the rows that matched. The running code is not touched |
rulec verify — Compare and replay |
| past records | Replay the rule over them. For a change, how many records move and by how much comes out before it ships. Which inputs move at all needs no records, only the two versions | rulec fixtures lint, then rulec replay / rulec diff — Compare and replay |
Who writes it — a person, an agent, and rulec
Today a rule sits in a spreadsheet, a published policy, a wiki page or somebody's head, and an
engineer rewrites it as a chain of ifs. rulec hands that rewrite to an agent, and changes
what the agent hands back: a rule a person can read, instead of code.
Indigo is the loop between the agent and rulec, and it runs without a person: the agent hands over the rule, rulec hands back what is wrong — where, how to fix it, and an input that shows it — and the agent fixes it and hands it over again. Amber is the detour through a person, who is asked only what cannot be derived from the source — "what is the fee for a small parcel going overseas?" — and answers with an amount or a rounding direction, never with code. What they read and check is a document rendered from the rule, with a page to try a case on.
The agent's procedure is For agents. The
agent skill ships in the repository
(how), rulec mcp offers the same commands as tools where there
is no shell (how), and findings come back as JSON whose codes and
shape stay put while the wording improves.
What gets proved, and what does not
Seven things are settled before anything is generated. Five are proved statically — every input matches some row, no input matches two, no row matches nothing, units are never confused, every intermediate fits in int64. One is a declaration that has to be there — how fractions are settled, because which way is right is a business decision. One is run — every worked example holds. If any of the seven cannot be shown, nothing is generated.
What is not proved matters just as much: that the rule matches reality, that the generated code answers like the rule — that is tested, byte for byte in each generated language, not proved — the row pairs the overlap proof could not reach, and that the checker itself is right. Where each layer stops is on What it proves and How it is checked.
What you can write in it, and what you cannot
A rule that decides one case, in one go, from flat facts, and hands back an amount, a yes/no, a class or an order: a tariff, a discount, a rate, an eligibility test, a classification, a routing decision, a statutory provision. Money is not required.
The language has two parents. The conditions come from decision tables, by way of DMN; a main
rule with its exceptions and provisos comes from law written as logic, by way of Catala. What
it leaves out — recursion, state, date arithmetic,
nested objects, and any cell that looks at two columns at once — is what keeps every check
decidable. A cell narrows its own column and nothing else, so a row is a box, and whether boxes
leave a gap or overlap can be computed exactly. weight × 10 > order total cannot be a cell;
named with a derive or a define, it becomes a column of its own.
Whether yours fits — five questions, and how rulec differs from DMN, rules engines and Catala — is on Does your rule fit.
Where to read next
| page | what is on it |
|---|---|
| Write a rule (.rule) | the language, from one table to exceptions, provisos and lists |
| What it proves | the seven checks, and how to read a diagnostic |
| Generate and call | the twelve targets, and the rule as an MCP tool or a service |
| Compare and replay | against what runs today, and against past records |
| How to use it, by role | a public rule, your own rule, a new one, and an API contract |
| Examples | rules transcribed from tariffs, terms and statutes |
| Does your rule fit | five questions, and what else is out there |