Skip to content

Customization

Appearance Rules control how nodes look on the Verilib graph: their fill color, shape, border, arrow style, status bar, corner dot, and text badge. Instead of one giant "everything at once" rule, Verilib splits rules into three layers — Property → Appearance → Values — so you can build up styling incrementally and reuse conditions across multiple visual channels.

This page explains the model, the rule expression language, the built-in defaults, how repo-level overrides via .verilib/config.json interact with rules you create in the app, and gives worked examples for a Lean + Rust formal-verification repo. It is the frontend counterpart to Atom statuses and colours: that page defines the canonical, VeriLib-wide bar/dot scheme the atomizer persists; this page covers the app's rule engine that lets a repo owner customize how those (and other) atom fields are rendered on top of it.

1. The mental model

Property "Blocked Theorem"
 ├─ Appearance: Shape
 │    └─ Value: status == "rejected" && language == "rust"  ==>  oval
 ├─ Appearance: Border
 │    └─ Value: status == "rejected" && language == "rust"  ==>  orange, solid
 └─ Appearance: Dot
      └─ Value: status == "rejected" && language == "rust"  ==>  red dot
  • Property — a named group of styling you're defining, e.g. "Blocked Theorem" or "Compilation status". The name is just a label for you (it shows up in the Legend); it doesn't affect matching.
  • Appearance — which visual channel this group of rules controls. There are seven: Shape, Fill, Border, Arrow, Bar, Dot, Letters. A Property can have at most one block of each kind (you can't add "Fill" twice to the same Property, but you can add Fill and Shape and Dot to the same Property).
  • Value rule — inside an Appearance block, one or more condition ==> value rows. Conditions are written in a small expression language (see §3). Rows are evaluated top to bottom and the first one whose condition is true wins — later rows in the same block are only used as a fallback for nodes that didn't match an earlier row.

A single Property is really just a convenient way to co-author several Appearance blocks that share the same intent. Nothing stops you from matching the same condition in one Property and adding "Fill" rules for it in a completely different Property — but grouping them together under one Property name keeps the editor (and the Legend) readable.

Which channel affects what

Appearance Affects
Shape The outline of the matching node (rounded rectangle, cut corner, oval, square)
Fill The node's body color
Border The node's border color and line style (solid / dashed / dotted)
Arrow The style of connector lines going out of the matching node (filled / open / hollow head)
Bar The thin status bar at the bottom of the node (color, or hidden entirely)
Dot A small color dot in the corner of the node — optional, pick "None" to hide it
Letters A short text badge on the node (up to 4 characters), either typed manually or auto-derived from the atom's statement type

Shape, Border, Dot and Letters describe the node itself. Arrow is the only channel that describes something else — the edges leaving that node.

2. Adding a property in the editor

  1. Open Edit Atom Rules on the repo.
  2. Click + Property and give it a name (e.g. Blocked Theorem).
  3. Click + Appearance and pick a channel from the dropdown (Shape, Fill, Border, Arrow, Bar, Dot, or Letters). Only channels you haven't already added to this Property show up in the list.
  4. Each Appearance block starts with one Value row. Click + Value to add more — useful when the same channel needs different outcomes for different conditions (e.g. a Dot that's red for one status and green for another).
  5. Repeat step 3 for any other channel this Property should also control (e.g. add both Shape and Border under "Blocked Theorem").
  6. Drag properties up/down in the list to change priority — see §4.

Worked example: "An oval with an orange border is a Theorem that is Blocked"

UI field Value
Property name Blocked Theorem
Appearance #1 Shape → value rule: status == "rejected" && statement_type == "theorem" ⟶ oval
Appearance #2 Border → value rule: status == "rejected" && statement_type == "theorem" ⟶ color #F99922, style solid

Because both rules share the same condition, Verilib merges them internally so the node ends up oval-shaped and orange-bordered whenever that condition is true.

3. The rule expression language

Conditions are written in CEL (Common Expression Language) — a small, safe boolean expression syntax. Every condition must evaluate to true or false.

Operators

Operator Meaning
==, != equals / not equals
&&, \|\| logical AND / OR
!(...) logical NOT — must wrap the whole comparison, e.g. !(language == "lean"). Writing !language == "lean" is invalid — ! binds to language alone, not to the comparison. Prefer language != "lean" when negating a single equality.
(...) grouping, to control precedence when combining && / \|\|
"..." string literals must be double-quoted, e.g. "rust" — bare words like rust are not valid CEL

Available fields

Field Type Description
disabled 0/1 1 if the atom is disabled
specified 0/1 1 if the atom is specified
translated 0/1 1 if the atom has been translated
validated 0/1 1 if specified and status is verified or transitively_verified
status_id number Raw numeric status id (see table below)
status string Status name — one of: initial, submitted, processing, verified, rejected, published, locked, awaiting_decision, appealed, disputed, specified, trusted, transitively_verified, unspecified
language string Source language — one of: dafny, lean, rocq, isabelle, metamath, rust, refinedc, python, kani, verus
prooflanguage string Proof language — same set of values as language
statement_type string e.g. theorem, lemma, definition, axiom, predicate, inductive, structure, proof, spec, method, function, instance, datatype — the exact list depends on what your repo contains
type string Atom type string, repo-dependent
identifier / full_identifier string The atom's name / fully-qualified name

There is no language_id, prooflanguage_id, or kind field. Those are the raw database columns; the rule engine exposes the human-readable language / prooflanguage / status names instead, so write language == "rust", not language_id == 6 or kind == "rust". status_id is the one exception where the raw numeric id is exposed directly (useful for matching several statuses by range, though status == "..." is usually clearer).

The right-hand panel of the editor ("Available fields") always shows the current, repo-specific list — including which statement_type / type values actually occur in your repo.

Numeric status ids (for status_id)

id name
-1 unspecified
0 initial
1 submitted
2 processing
3 verified
4 rejected
5 published
6 locked
7 awaiting_decision
8 appealed
9 disputed
11 specified
12 trusted
14 transitively_verified

Common mistakes

  • Negating with ! on a comparison — write language != "lean" or !(language == "lean"), not !language == "lean".
  • Unquoted strings — status == rejected fails; it must be status == "rejected".
  • Using the _id suffix — use language/prooflanguage/status (names), not language_id/prooflanguage_id (these columns aren't exposed to rules).
  • Empty condition — a Value row with a blank expression is invalid and blocks saving; every row needs a real condition, even if it's just true (matches everything — handy as a catch-all row placed last in a block).

4. How matching actually works

Within one Appearance block, rows are evaluated top-to-bottom and the first matching row wins — rows below it are ignored for that node.

Across Properties, the same first-match-wins logic applies per channel, using the order Properties are listed in the editor (drag to reorder). So if two different Properties both define a Fill rule and both conditions are true for a given node, the Property that's higher in the list wins for Fill — completely independently of which Property wins for Shape or Dot.

Two channels behave slightly differently from the rest, which is worth knowing when a Dot or Letters badge doesn't show up as expected:

  • Fill, Shape, Border, Arrow lock onto the first matching row, full stop — even if that particular row didn't explicitly set that field (e.g. a Shape block whose matched row didn't override shape falls back to the default rounded-rect, rather than checking further rows).
  • Dot and Letters are more forgiving: if the first matching row doesn't specify a dot/letters value, evaluation keeps checking later matching rows until one actually provides a value (or gives up and shows nothing).

In practice, keep it simple: put your most specific conditions first, followed by broader "fallback" conditions, both within a block and by dragging important Properties higher in the list.

5. Value reference

Shapes: rounded-rect (default), cut-corner, oval, square

Border styles: solid (default), dashed, dotted

Arrow styles: filled (default), open, hollow

Dot: any color, or "None" to hide it (a node has no dot unless a rule gives it one)

Bar: a color for the status bar, or "hide" to remove the bar entirely

Letters: either type up to 4 characters manually, or toggle "Auto" to derive a short badge from the atom's statement_type:

statement_type Auto badge
def / definition Def
abbrev Abbr
axiom Axm
datatype Data
exec Exec
fun / function Func
ghost function GFun
ghost predicate GPrd
inductive Ind
instance Inst
lemma Lem
method Mthd
molecule Mol
opaque Opq
opaque function OpFn
predicate Pred
projection Proj
proof Prf
spec Spec
structure Stru
theorem Thm

6. Built-in defaults

If a repo has no custom rules at all, Verilib falls back to these, evaluated top to bottom:

Property Condition Fill Notes
Disabled disabled == 1 gray #A9AAAD status bar hidden
Trusted status == "trusted" purple #9B59B6
Verified specified == 1 && status == "verified" green #45CE17
Transitively Verified specified == 1 && status == "transitively_verified" dark green #1A7A1A
Specified specified == 1 blue #4E98F3
Translated translated == 1 yellow #E8BA00
Unspecified (catch-all) true white #FFFFFF gray solid border, status bar hidden

Once you add even one custom rule in the app, this list stops applying — your rules become the source of truth for the channels they cover. Channels you never add stay at their neutral default (no shape override → rounded-rect, no dot rule → no dot, etc.) rather than silently falling back to this table.

These defaults are the app-side rendering of the same fields Atom statuses and colours defines at the atomizer level (verification-status, untracked, kind, language) — the rule engine here is what a repo owner uses to override that default rendering.

7. Overriding rules from your repo: .verilib/config.json

Verilib also supports defining rules inside the repository itself, so styling can travel with the code and be reviewed via normal pull requests instead of being a setting hidden in the web UI.

File location and format

Create .verilib/config.json at the root of your repository:

{
  "color_rules": [
    { "expr": "language == \"rust\" && status == \"rejected\"", "color": "#BB1416" },
    { "expr": "prooflanguage == \"lean\" && validated == 1",    "color": "#45CE17" },
    { "expr": "language == \"rust\" && status == \"verified\"", "color": "#4E98F3" }
  ]
}
  • color_rules is an array of { "expr": "...", "color": "#RRGGBB" } objects, evaluated first-match-wins in listed order — same expression language as §3.
  • Both expr and color are required on every entry, or the entire file is rejected (an all-or-nothing check — one bad rule discards the whole set, it does not just skip that one entry).
  • Only expr and color are read. Even if you add shape, borderColor, dotColor, etc. to an entry, they are silently ignored — file-based config currently controls Fill color only. Use the in-app editor for shape/border/arrow/bar/dot/letters rules.
  • The file is picked up during atomization (when the repo is synced / re-imported) — editing it doesn't take effect instantly, only on the next sync.

Precedence: app rules vs. repo rules

Rules you create in the Edit Atom Rules modal ("web" rules) and rules that came from .verilib/config.json ("repo" rules) are combined as:

[ ...web rules, ...repo rules ]

and evaluated first-match-wins as one list. Web (in-app) rules always take priority over repo-file rules for any condition they both match — repo rules are effectively a lower-priority baseline. This is why repo rules show up as read-only in the right-hand panel of the editor: you can see what the repository defines, but you edit web rules, not repo rules, from the UI. To change repo-defined styling, edit .verilib/config.json and re-sync the repository.

These assume a repo that verifies Rust code with Lean proofs (language == "rust", prooflanguage == "lean"), but the same patterns apply to any language pair Verilib supports.

1. Color nodes by proof status

Property: Proof status
Appearance: Fill
  language == "rust" && status == "verified"              ==> #45CE17 (green)
  language == "rust" && status == "rejected"               ==> #BB1416 (red)
  language == "rust" && status == "processing"             ==> #E8BA00 (yellow)
  true                                                      ==> #D9DADE (gray, catch-all)

2. Flag rejected theorems with a distinct shape + border (the "Blocked Theorem" pattern)

Property: Blocked Theorem
Appearance: Shape
  status == "rejected" && statement_type == "theorem"      ==> oval
Appearance: Border
  status == "rejected" && statement_type == "theorem"      ==> orange #F99922, solid

3. A compilation-status dot that ignores Lean proof obligations

Property: Compilation status
Appearance: Dot
  status == "rejected" && language == "rust"                ==> #BB1416 (red)
  status == "processing" && language == "rust"               ==> #E8BA00 (yellow)
  status == "verified" && language == "rust"                 ==> #45CE17 (green)
  prooflanguage == "lean"                                     ==> None

Because Dot rules keep scanning past matches with no dot value (§4), you can add a broad prooflanguage == "lean" ==> None row at the end without worrying it will mask the more specific Rust rules above it — those are checked first and already provide a value.

4. Distinguish trusted axioms from proven lemmas

Property: Axiom vs. Lemma
Appearance: Letters
  statement_type == "axiom"                                   ==> "Axm" (manual) or Auto
  statement_type == "lemma"                                   ==> "Lem" (manual) or Auto
Appearance: Border
  statement_type == "axiom"                                   ==> dashed, gray — visually flags "trust me" axioms

5. Highlight cross-language proof obligations

Property: Lean-verified Rust
Appearance: Bar
  language == "rust" && prooflanguage == "lean" && validated == 1  ==> bar color #45CE17
  language == "rust" && prooflanguage == "lean" && validated == 0  ==> bar color #E8BA00
Appearance: Arrow
  language == "rust" && prooflanguage == "lean"                    ==> hollow

This gives every Rust atom backed by a Lean proof a distinct outgoing connector style, independent of whatever Fill/Shape rules color the node itself.

6. Repo-wide baseline via .verilib/config.json, refined per-viewer in the app

Ship a conservative default with the code:

{
  "color_rules": [
    { "expr": "language == \"rust\" && status == \"rejected\"", "color": "#BB1416" },
    { "expr": "true", "color": "#D9DADE" }
  ]
}

Then, in the app, add a Property with Shape/Dot/Border rules for your personal review workflow — those web rules layer on top and always win over the repo baseline (§7), without needing write access to the repository to experiment.

9. FAQ / troubleshooting

My Dot never shows up. Check that the row's expression actually evaluates true for that node (use the "Available fields" panel to confirm the exact field names/values your repo uses), and that you didn't accidentally set the dot color to "None" on the matching row.

I set a rule in .verilib/config.json and nothing changed. File-based rules apply on the next atomize/sync of the repo, not instantly — and remember only expr/color are honored from the file. Also check that a web rule with a higher-priority matching condition isn't overriding it (§7) — repo rules are read-only in the UI for this reason.

Adding a row broke validation / I can't save. Every Value row needs a non-empty expression that parses as CEL and returns true/false. The most common culprits are unquoted strings (status == rejected instead of "rejected") and negation placement (!language == "lean" instead of language != "lean").

Two Properties both try to color the same node differently. First-match-wins applies per channel across the whole rule list, ordered by how Properties are arranged in the editor. Drag the Property you want to take priority higher in the list.