Skip to content

How to use guided synthesis to produce a verified candidate

Audience: developer whose RULE-only block exceeds the bounded synthesiser's search budget and wants to provide a hand-written or LLM-generated implementation that is subsequently verified by a bounded model checker.\ Prerequisites: familiarity with LoLa RULE and ASSUME, the bounded synthesiser, the lola guided CLI, and either Kani (Rust) or CBMC (ST).\ Concept: Guided synthesis and EXTERN — same warrant, different source\ Reference: GuidedSynthesisWarrant

When to use this

The bounded synthesiser inside compile_source searches all BOOL candidate expressions up to a fixed node budget (default: 32 nodes, 16 operators). For blocks with a handful of BOOL outputs and simple RULE constraints, this is enough.

Use guided synthesis when:

  • The synthesiser reports synthesis-bound-exhausted.
  • The output requires non-trivial arithmetic or array comparisons (e.g. a resource-ranking scheduler, a priority arbiter with tie-breaking).
  • You have a correct algorithm in mind but want to prove it rather than just assert it.

The legacy free-form Rust/Kani and ST/CBMC request builders refuse MATHREAL/LREAL outputs. A bounded model checker proves such a candidate over machine floating-point arithmetic, but a LoLa RULE over reals is an exact ℝ statement; the two theorems differ exactly by the roundoff the checker cannot see. GS-v2-N therefore takes a different path: the candidate is a narrow LoLa realization, the ordinary compiler proves it over ℝ and emits both machine backends, and acceptance additionally requires SNC-proved binary64 envelopes. See examples/guided/affine_real_gs.lola for the first slice and examples/algorithms/lm_step/ (LM_Cramer2x2) for the worked example of that split.

Overview

1. Write a RULE-only spec (.lola)
2. lola guided <spec> --out DIR                       →  proof_request.json
3. LLM fills the hole (--agent, or by hand)           →  candidate.json
4. lola guided <spec> --out DIR \
       --verify-candidate DIR/candidate.json \
       --proof kani --accept                          →  acceptance.json
5. compile_source(..., guided_synthesis_warrants={"Block": warrant})

Steps 3 and 4 iterate until the proof succeeds.

Stateful GS-v2-S

For a direct register implementation, LoLa itself defines the normative transition. lola guided exposes immutable pre-state and asks the candidate to return output plus next state. The proof backend separately checks the default initial state and one inductive transition.

Init(S) => Inv(S)
Inv(S) AND ASSUME(I) AND REQUIRE(I) AND Candidate(I,S)=(O,S')
    => T_LoLa(I,S,O,S') AND Inv(S')

The first slice covers DebounceGs and HysteresisIntGs on both Rust/Kani and ST/matiec/CBMC. Replayable candidates are in examples/guided/candidates/. Timers, arrays, derived values, composition, REAL/LREAL, WSTRING, EXTERN, and input-dependent invariants are intentionally rejected.

Output-dependent contract reads (GS-v2-CDEF-1)

Contracts may read a statically bounded array through a result index when the index bounds are established independently:

RULE idx >= 0;
RULE idx <= 3;
RULE ALL(i IN 0..3 : a[i] <= a[idx]);

The compiler creates and proves a separate definedness obligation for a[idx], then schedules that check before the indexed rule in both Kani and CBMC. The indexed rule itself is never accepted as proof that its index is safe. Indexed ASSUME/REQUIRE clauses are scheduled separately: total premises establish their bounds before the partial premise is evaluated, and a later output guarantee cannot make a premise defined. Dynamic writes and state-array indexing remain outside this slice. A contract that also needs division/modulo definedness is rejected until those obligations share the same phase-aware replay model. The compiler-owned bounds proof has a fixed timeout; unknown, timeout, and solver exceptions abort candidate generation and cannot produce an acceptance claim. See examples/guided/arg_max4_gs.lola for the end-to-end Rust and ST example.

Semantic array contracts (GS-v2-C)

A sorting requirement can state meaning rather than an implementation network:

RULE SORTED(s);
RULE PERMUTATION_OF(s, a);

SORTED(s) means nondecreasing logical index order. PERMUTATION_OF(s, a) compares exact multiplicities, including duplicates; it is not a sum, XOR, or hash fingerprint. Both arrays must have identical bounds and machine-integer element types. The compiler lowers these predicates from one canonical definition into the normal Z3 model, Kani, and CBMC, and binds their canonical text into the proof request and warrant. Negative/nonzero lower bounds retain their logical meaning.

The candidate remains an ordinary implementation and contains no privileged sorting operation. examples/guided/sort4_semantic_gs.lola ships replayable Rust and ST candidates plus adversarial tests for constant-fill, unchanged, and duplicate/drop implementations. If indexed clauses are mixed into the contract, CDEF-1 proves and schedules their definedness before the candidate executes.

Exact-real candidates with machine envelopes (GS-v2-N)

The first numeric slice accepts one combinational, RULE-only block with scalar REAL/LREAL ports and direct LoLa output assignments. It deliberately does not accept free Rust/ST bodies, state, arrays, wiring, composition, timers, or externs. Its candidate-expression allowlist also rejects PRE, DT, HELD/ELAPSED, calls, conversions, indexing, and aggregates before the ordinary compiler or SNC runs. Template parameters and continuous references are outside the specification surface as well.

from lola.guided_numeric import verify_numeric_candidate

proof = verify_numeric_candidate(source, "y := 0.1 * x + 0.2;")

Acceptance is conjunctive: the ordinary compiler must prove the candidate against every exact-real RULE, and snc.view(compilation) must return Proved for every REAL/LREAL output derived from the candidate ABI. Any Absent rejects and reports its diag_ref. The proof retains the original immutable SNC view and ErrorEnvelope objects; it neither reconstructs envelopes nor invents replacement warrant identities. SNC_API_VERSION is checked for compatibility but remains outside theorem-bearing digests. Rust f64 and ST LREAL are then emitted from the same accepted compilation.

Step 1 — Write a RULE-only specification

Write a FUNCTION_BLOCK with ASSUME and RULE inside IMPLEMENTATION. Leave the outputs without any := definition.

FUNCTION_BLOCK PumpBank
VAR_INPUT
    demand : INT;
    ok     : ARRAY[0..2] OF BOOL;
    hours  : ARRAY[0..2] OF DINT;
END_VAR
VAR_OUTPUT
    run : ARRAY[0..2] OF BOOL;
END_VAR
IMPLEMENTATION
    ASSUME demand >= 0;
    ASSUME demand <= 1;
    ASSUME COUNT(i IN 0..2 : ok[i]) >= demand;
    RULE COUNT(i IN 0..2 : run[i]) = demand;
    RULE ALL(i IN 0..2 : (NOT run[i]) OR ok[i]);
    RULE ALL(i IN 0..2 : ALL(j IN 0..2 :
        (NOT (run[i] AND ok[j] AND (NOT run[j]))) OR (hours[i] <= hours[j])
    ));
END_IMPLEMENTATION
END_FUNCTION_BLOCK

This block has three RULEs: exactly demand pumps run, only healthy pumps run, and the running pump has the fewest accumulated hours.

Step 2 — Build the proof request

lola guided pump_bank.lola --out build/proof/

This writes build/proof/proof_request.json, which contains the canonical block contract (inputs, outputs, types, ASSUME and RULE texts) and the Kani proof skeleton (candidate.creusot.rs). The request is immutable: every downstream step is tied to its SHA-256.

Step 3 — Obtain a candidate

Either:

a) LLM-assisted (automated)

lola guided pump_bank.lola --out build/proof/ --agent claude

This sends the rendered prompt from proof_request.json to Claude and writes the candidate body to build/proof/candidate.json. The proposal is untrusted until step 4 replays it under the proof backend.

b) Hand-written

Open build/proof/candidate.creusot.rs, locate the // CODEX_CANDIDATE_BODY marker, and replace it with your implementation. Write the body in safe Rust; the harness already maps LoLa inputs to the Rust struct fields.

Example body for PumpBank:

let run0 = input.demand >= 1 && input.ok[0]
    && (!input.ok[1] || input.hours[0] <= input.hours[1])
    && (!input.ok[2] || input.hours[0] <= input.hours[2]);
let run1 = input.demand >= 1 && input.ok[1]
    && (!input.ok[0] || input.hours[1] < input.hours[0])
    && (!input.ok[2] || input.hours[1] <= input.hours[2]);
let run2 = input.demand >= 1 && input.ok[2]
    && (!input.ok[0] || input.hours[2] < input.hours[0])
    && (!input.ok[1] || input.hours[2] < input.hours[1]);
PumpBankOutputs { run: [run0, run1, run2] }

Step 4 — Accept (prove) the candidate

lola guided pump_bank.lola --out build/proof/ \
    --verify-candidate build/proof/candidate.json \
    --proof kani --accept

What this does:

  1. Inserts the candidate body into the Kani proof harness.
  2. Runs Kani over all input combinations (symbolic exhaustion).
  3. If Kani reports VERIFICATION SUCCESSFUL: writes build/proof/acceptance.json (a GuidedSynthesisWarrant) and build/proof/candidate_accepted.rs.

acceptance.json is a content-addressed receipt:

{
  "schema": 3,
  "block": "PumpBank",
  "target": "rust",
  "declaration_sha256": "41ddb447...",
  "semantic_contract_sha256": "7a26f15d...",
  "candidate_body_sha256": "9f3c2b1a...",
  "proof_backend": "kani",
  "proof_source_sha256": "e72a4f88...",
  "rules": [
    "COUNT(i IN 0..2 : run[i]) = demand",
    "ALL(i IN 0..2 : (NOT run[i]) OR ok[i])",
    "..."
  ]
}

The declaration_sha256 is a SHA-256 of the block's canonical contract (inputs, outputs, ASSUME, RULE, synthesis targets). It is stable across formatting and comment changes but changes whenever the contract itself changes. Its embedded semantic_contract_sha256 also binds the canonical expanded AST meaning of semantic predicates such as SORTED and PERMUTATION_OF, so changing their compiler definition invalidates an old acceptance even when the source spelling is unchanged.

If Kani finds a counterexample: examine the failing model, correct the candidate body, and re-run step 4.

Step 5 — Compile with the warrant

Load the acceptance receipt into a GuidedSynthesisWarrant and pass it to compile_source:

import json
from lola import compiler
from lola.guided_synthesis import make_guided_synthesis_warrant

acceptance = json.loads(open("build/proof/acceptance.json").read())
warrant = make_guided_synthesis_warrant(acceptance)

comp = compiler.compile_source(
    source,
    guided_synthesis_warrants={"PumpBank": warrant},
)
assert comp.report.ok

When guided_synthesis_warrants contains an entry whose declaration_sha256 matches the current source contract, compile_source:

  1. Skips CEGIS synthesis — the warrant discharges the RULE proof obligations.
  2. Inserts stub derived entries so the sema and composition passes see defined outputs.
  3. Records the warrant in program.assurance.guided_synthesis_warrants.

The assurance report will show:

guided_synthesis_warrants:
  PumpBank:
    block: PumpBank
    proof_backend: kani
    declaration_sha256: 41ddb447...
    candidate_body_sha256: 9f3c2b1a...
    ...

Failure modes

declaration_sha256 does not match

The acceptance was produced from a different source contract. Either the source changed after acceptance (re-run steps 2–4), or the wrong acceptance file was passed.

must be a GuidedSynthesisWarrant

The dict value is not a GuidedSynthesisWarrant. Use make_guided_synthesis_warrant to convert an acceptance dict.

synthesis-bound-exhausted (no warrant supplied)

The bounded synthesiser could not find a solution within the default budget and no warrant was provided. Either provide a warrant from a completed acceptance, or increase the synthesis bound via SynthesisBound.

Connecting to the runtime

The candidate_accepted.rs file is the Rust implementation the Kani proof covered. Include it in your NRA Rust project alongside the generated LoLa scaffolding:

// In your project's main.rs or lib.rs:
include!("build/proof/candidate_accepted.rs");

The generated LoLa Rust scaffolding calls candidate(input) from candidate_accepted.rs.

For ST: candidate_accepted.st contains the equivalent structured-text body; link it into your MATIEC project.

See also