Reading Between The Lines of Code

int check(int *a, int *b, int n) {
  /* You are not expected to understand this. */
  for (int i = 0; i < n; i++) {
    if (a[i] != b[i])
      return 0;

READING

between
the lines
of

CODE

  }
  // DO NOT TOUCH. Nobody knows why this works.
  return 1;
}

// Dr. Elizabeth Polgreen · University of Edinburgh

// Work by Owain Parry, Guy Frankel and Leiqi Ye

We all write code.

Increasingly, AI writes it for us.

Formal verification lets computers check that code is correct.

Hand-drawn stick figure frustrated at a computer desk

Hand-drawn robot typing at a computer desk

2

Why don’t we verify everything?

The standard reason

“It doesn’t scale.”

Maybe solved now?

LLMs + interactive theorem provers can find the proofs.

(…if you have enough money)

3

But the question

“What should we be verifying?”

is still really hard to answer.

4

Most code is legacy code

Written by someone who left the company years ago.

Limited documentation.

Maybe it has tests.

Maybe it doesn’t.

?

5

Who knows what they intended?

// No idea what this does.
// But if you delete it, everything breaks.
// DO NOT TOUCH.
legacy_init(cfg, 0x7f, NULL);

legacy.c

legacy.rs

Does it do the same thing?

6

Now the code is written by LLMs

what I actually want

prompt

fn f(x: i32) {
  // ...
  // ...
}

① Did they say what they meant?

② Did the LLM do what they asked?

7

LLMs are optimising our code

original

for (i = 0; i < n; i++)
  for (j = 0; j < n; j++)
    c[i] += A[i][j] * b[j];

optimised: 12× faster!

/* tiled, vectorised, unrolled */
__m256 acc = _mm256_setzero_ps();
for (jj = 0; jj < n; jj += 64)
  ...

≡ ?

How do we know the optimised code still does the right thing?

8

We need formal specifications

Hand-drawn stick figure with head on the desk in despair

Writing them by hand is expensive and hard.

In hardware, writing specifications can take up to 60–70% of development time.

a <= result

d <= result

result == 0

Can we generate them automatically?

9

Specification Mining

Hardware

Symbolic synthesis

SMART · MAPminer

Software

int check(int *a,
  int *b, int n) {
  ...
}

LLMs + verifiers

AutoC2VR

10

Specification Mining

Hardware

Symbolic synthesis

SMART · MAPminer

Software

int check(int *a,
  int *b, int n) {
  ...
}

LLMs + verifiers

AutoC2VR

11

Hardware bugs are expensive

A bug found after fabrication is VERY expensive

e.g. Intel’s Pentium FDIV bug (1994): a ~$475M write-off.

And LLMs are starting to optimise hardware designs too.

e.g. AlphaEvolve (Google DeepMind, 2025) proposed a Verilog rewrite of an arithmetic circuit for Google’s TPUs.

So we want specifications.

12

Existing approaches

Templates

a == b
a |-> ##1 b
a <= b

Limited expressivity, and really, really big sets of assertions (most of which don’t hold)

LLMs

Unreliable, and can’t typically reason well about weird edge cases

Humans

Hand-drawn stick figure in despair at a desk

Expensive… and they get sad if you give them too many boring, hard tasks

We’re going to use formal synthesis instead.

13

The problem

Given a hardware design H, find assertions that are:

Valid: true in every reachable state of H

Formally, solve the synthesis problem:

∃Φ. ∀ inputs .H ⊨ Φ

INIT

reachable states

Φ holds

14

The problem

Given a hardware design H, find assertions that are:

Valid: true in every reachable state of H

Meaningful: not vacuous; compact; more readable than the design itself

Formally, solve the synthesis problem:

INIT

reachable states

α holds

BAD

15

∃Φ. ∀ inputs .H ⊨ Φ

Example: the max of three inputs

// return the max of three inputs
module max3 (
  input  [7:0] a, b, c,
  output [7:0] result );
  wire [7:0] d;
  assign d = (a >= b) ? a : b;
  assign result = (d >= c) ? d : c;
endmodule

Assertions we’d like to find:

assert property (a <= result);

assert property (d <= result);

16

Synthesis from examples

Encoding H ⊨ α directly means unrolling the transition system. Instead, we use examples:

Positive examples

reachable states, from simulation traces.

Negative example

a random unreachable state, checked by a model checker.

Counterexamples

reachable states the verifier finds that α gets wrong: added to the positives

∃Φ . (∀s ∈ S+ . Φ(s+) = ⊤) ∧ Φ(s-) = ⊥

(set-logic BV)
(synth-fun inv ((d (_ BitVec 8))
      (result (_ BitVec 8))) Bool)
; from the simulation trace
(constraint (= (inv #142 #148) true))
(constraint (= (inv #172 #179) true))
; from a negative state
(constraint (= (inv #111 #2) false))
(check-synth)

A (simplified) SyGuS query for d and result in max3

17

SMART

Simulation traces
→ positive examples

Random unreachable state
→ negative example

SYNTHESIZE

enumerate from grammar (cvc5)

VERIFY

model checker (EBMC, k-induction)

fails: counterexample trace → more positive examples

holds: keep φ, then move on to other variables

18

φ

Too many variables

Enumerative synthesis scales exponentially with the number of variables, and real designs have thousands of signals.

a

b

c

d

rst

en

cnt

s3

req

…

U0 = {a, d, cnt}

U1 = {b, rst, s3}

U2 = {c, en, req}

Random small subsets of the variables, of size round(2.7 + 2.0 log₁₀ |V|).

Found Φ over {a, d}? Remove a and d from current subset, so the next assertion talks about other signals.

A fresh random negative example per call pushes each query towards a different bad behaviour.

19

SMART: the full loop

Simulation traces
→ positive examples P

Random unreachable state
→ negative example

Pick variable subset

same subset

SYNTHESIZE

φ over variable subset

VERIFY

H ⊨ φ? (EBMC)

holds: add φ to Φ, remove var(φ) from variable subset and synthesize again

no φ exists (or var subset empty)

fails: counterexample states join P

next subset

Output: Φ

stop when subsets run out, on timeout, or |Φ| = Φmax

20

Temporal properties

Some bugs are about what happens next: broken state machines, non-atomic access checks, …

now (t)

a, b, req, …

k clock cycles

later (t + k)

a′, b′, ack′, …

Copy every variable, then synthesise implications:

Expr ::= Bool(now) ⟹ Bool(later)

assert property (req |-> ##1 ack);

“if req now, then ack one cycle later”

21

Temporal negative examples

A negative example is now a pair of states: (now, later)

→

an unreachable state now, and a state reachable from it later

→

a reachable state now, and a later state that can’t follow it

Both states unreachable? Too imprecise to refine the assertions, so we don’t use those pairs.

Verification

Temporal assertions are checked with bounded model checking (EBMC), so they come with bounded guarantees.

22

Is a specification any good?

A good specification should notice when the design changes.

original H

assign d = (a >= b) ? a : b;

H ⊨ Φ

mutant H′

assign d = (a <  b) ? a : b;

H′ ⊭ Φ detected!

MD-rate = |{ H′ ∈ M : H′ ⊭ Φ }| / |M|

23

Generating mutants

Where in the Verilog

Rewrite to

Example

Gates: and, or, nand, nor, xor, xnor, not, buf

another gate

and(y, a, b) → nor(y, a, b)

Bitwise operators: &, |, ^

another bitwise op

x & y → x | y

Arithmetic operators: +, −, *, /, %

another arithmetic op

a + b → a * b

Relational operators: ==, !=, <, >, <=, >=

another comparison

a >= b → a < b

Boolean variables

its negation

en → !en

Bit-vector literals

a random value

8'd5 → 8'd173

Each operator: apply one applicable rule, chosen at random

Each boolean variable: negate it

Each literal: replace it with a random value

Each mutant changes the design in exactly one place. It is detected if H ⊨ A but H′ ⊭ A (EBMC, k-induction).

24

SMART: results

Average mutation-detection rate, 38 Verilog benchmarks (ISCAS’85, ISCAS’89, Ibex RISC-V)

Bar chart of average mutation-detection rate: HARM 22.3%, GoldMine 4.3%, SMART 52.2%, SMART with temporal assertions 56.4%

50

22.3%

4.3%*

52.2%

56.4%

HARM

GoldMine

SMART

SMART + LTL

*GoldMine only supports the 4 behavioural benchmarks.

100%

of SMART’s assertions are formally verified (HARM: 8.4%)

>50×

fewer assertions than HARM (943 vs. 54,674 on average)

≈2×

mutation detection from counterexamples (63.1% with vs. 32.1% without)

25

SMART: are the assertions correct?

Verification-correctness (VC) rate per benchmark: the share of generated assertions that actually hold

Bar chart from the SMART paper: VC rate per benchmark for GoldMine, HARM and SMART (LTL2). SMART is 100% everywhere; HARM is mostly low; GoldMine only has bars on four behavioural benchmarks.

Every SMART assertion holds. Most of HARM’s don’t.

26

SMART: do the assertions catch mutants?

Mutation-detection (MD) rate per benchmark

Bar chart from the SMART paper: MD rate per benchmark for GoldMine, HARM and SMART (LTL2). SMART is highest on almost every benchmark.

SMART matches or beats related work on 36 of 38 benchmarks.

27

…but it’s slow

SMART solves one synthesis problem at a time: on average ~31 minutes per benchmark, and over 6½ hours on the largest.

How can we run in parallel without duplicating work across threads?

assert property (ADDVG3VCNVOR1NF == S3);
assert property (CNTVCON1 == S3);
assert property (ADDVG3VCNVOR1NF == CNTVCON1);
assert property (ADDVG3VCNVOR1NF == CNTVCON1);

← implied by the first two

← exact duplicate

Which variables should each thread look at?

28

I found CNTVCON1 == S3!

…so did I.

Which variables should we look at next?

Nobody has constrained x₁ yet. Look there!

THREAD 1

Hand-drawn stick figure shrugging, thread 2

THREAD 2

Hand-drawn stick figure thinking, the mUS

COMPUTE mUS

29

Where should we look next?

Assumption

A variable the specification doesn’t constrain yet probably should be constrained by a good specification.

Insight

A minimal satisfying assignment tells us which variables the specification doesn’t care about.

30

Minimal satisfying assignments

Φ = (x₂ ∨ x₃) ∧ x₄ over {x₁, x₂, x₃, x₄}

x₁

x₂

x₃

x₄

x₂ = ⊤

x₄ = ⊤

x₁

x₃

mSA: the fewest variables we must fix to make Φ true, whatever the rest are

mUS: everything else, the largest X such that ∀X. Φ is still satisfiable

x₁ isn’t constrained at all, so mine new assertions over {x₁, x₃}

31

Finding an mUS

MINIMAL HITTING SET

H: a variable from every predicate

GUESS

X = free(Φ) \ H

CHECK

is ∀X. Φ satisfiable?

UNSAT CORE C

add a hitting set of C to H

unsat

sat

mUS = X

Greedy hitting set: take the variables that appear in the most predicates first.

∀ distributes over ∧, so the unsat core points at the predicates to blame.

In practice the core is usually one predicate: we add one variable at a time.

32

Round 1 · step 1: hitting set

1 · HITTING SET

2 · GUESS

3 · CHECK

4 · UNSAT CORE

Φ =

φ₁ : a ∨ b

∧

φ₂ : b = c

a

b

c

d

b

in φ₁

in φ₁ and φ₂

in φ₂

in neither

■ in H: the spec constrains it

■ in X: guessed to be free

A hitting set H contains at least one variable from every predicate.

Greedy: pick the variable that appears in the most predicates first.

b appears in both φ₁ and φ₂, so b on its own hits every predicate.

H = {b}

Our first guess at the variables the spec constrains.

33

Round 1 · step 2: guess the mUS

1 · HITTING SET

2 · GUESS

3 · CHECK

4 · UNSAT CORE

Φ =

φ₁ : a ∨ b

∧

φ₂ : b = c

a

b

c

d

a

c

d

in H

■ in H: the spec constrains it

■ in X: guessed to be free

Guess: every variable not in H is unconstrained.

X = free(Φ) \ H = {a, c, d}

To test the guess, ask: is there a value of b that makes Φ true for every a, c and d?

∀a, c, d . (a ∨ b) ∧ (b = c) satisfiable?

34

Round 1 · step 3: check the guess

1 · HITTING SET

2 · GUESS

3 · CHECK

4 · UNSAT CORE

Φ =

φ₁ : a ∨ b

∧

φ₂ : b = c

a

b

c

d

■ in H: the spec constrains it

■ in X: guessed to be free

∀a, c, d . (a ∨ b) ∧ (b = c)

Try b = true:

φ₁ = a ∨ true: holds for every a

φ₂ = (true = c): fails when c = false

Try b = false:

φ₁ = a ∨ false: fails when a = false

No value of b works: unsat.

35

Round 1 · step 4: find the culprit

1 · HITTING SET

2 · GUESS

3 · CHECK

4 · UNSAT CORE

Φ =

φ₁ : a ∨ b

∧

φ₂ : b = c

φ₂ : b = c

a

b

c

d

c

■ in H: the spec constrains it

■ in X: guessed to be free

∀ distributes over ∧, so test each predicate on its own:

∀a . (a ∨ b)

satisfiable (take b = true)

∀c . (b = c)

unsatisfiable on its own: the unsat core is {φ₂}

Hit the core with a variable that isn’t already in H: that’s c.

H = {b, c}: go round the loop again

36

Round 2 · guess and check again

1 · HITTING SET

2 · GUESS

3 · CHECK

4 · UNSAT CORE

Φ =

φ₁ : a ∨ b

∧

φ₂ : b = c

a

b

c

d

a

d

H = {b, c} from round 1

■ in H: the spec constrains it

■ in X: guessed to be free

X = free(Φ) \ {b, c} = {a, d}

∀a, d . (a ∨ b) ∧ (b = c)

Try b = c = true:

φ₁ = a ∨ true: holds for every a

φ₂ = (true = true): holds

d doesn’t appear at all

Satisfiable: the guess X = {a, d} is right.

37

The result

1 · HITTING SET

2 · GUESS

3 · CHECK: sat

4 · UNSAT CORE

Φ =

φ₁ : a ∨ b

∧

φ₂ : b = c

a

b = ⊤

c = ⊤

d

mUS

mSA

mUS

mSA: σ = {b ↦ true, c ↦ true}, the variables the spec constrains

mUS: {a, d}, the variables it doesn’t

Once b is true, the spec says nothing about a. And d is never mentioned at all.

Next round: mine new assertions over {a, d}

38

MAPminer

new in MAPminer

COMPUTE mUS

under-specified variables

PARTITION

into k small variable sets

SYNTHESIZE

thread 1

SYNTHESIZE

thread 2

SYNTHESIZE

thread 3

SYNTHESIZE

thread k

MINIMISE

drop redundant assertions

repeat until no new assertions, or the mUS stops changing

39

MAPminer: results

Average mutation detection, 38 benchmarks

Bar chart of average mutation-detection rate: HARM 19.0%, SMART 55.3%, MAPminer 71.2%

19.0%

55.3%

71.2%

HARM

SMART

MAPminer

MAPminer runtime on c1355 (588 variables)

Bar chart of MAPminer runtime on c1355 by thread count: 2 threads 3443 s, 4 threads 2865 s, 8 threads 1946 s, 16 threads 1346 s, 32 threads 979 s, 64 threads 678 s

3,443s

2,865s

1,946s

1,346s

979s

678s

2

4

8

16

32

64

threads

All assertions formally verified (HARM: 15.6%) · 3,543 assertions on average vs. 54,806 for HARM · 5× faster from 2 to 64 threads, same quality

40

MAPminer keeps finding assertions

Line chart from the MAPminer paper for s344: MD rate against assertion count. HARM flattens near 12% after about 20 assertions, SMART plateaus near 60% after about 110, and MAPminer keeps rising past 75%.

s344: a 4×4 add-shift multiplier (ISCAS’89)

HARM stops improving after ~20 assertions: it has run out of templates.

SMART plateaus around 60% after ~110: random variable choice stops finding new relations.

MAPminer keeps climbing past 75%.

41

MAPminer: mutation detection

MD rate per benchmark: MAPminer vs SMART vs HARM (12-hour timeout, 32 threads)

Bar chart from the MAPminer paper: MD rate per benchmark for MAPminer, SMART and HARM. MAPminer is highest on most benchmarks.

71.2% on average, vs 55.3% for SMART and 19.0% for HARM

The biggest gains are on structural (gate-level) designs: 76.9% vs 59.6%.

42

Case study: a secure cache

Cache designs for memory isolation (PLRU and NRU replacement). Proving their end-to-end security property needs auxiliary invariants, normally written by experts.

Approach

PLRU

NRU

Unbounded?

k-induction + MAPminer invariants

141 s

131 s

yes

k-induction + manual invariants

days

days

yes

BMC (depth 20)

8,743 s

10,756 s

no

PDR

1,450 s

timeout

PLRU only

43

The cache’s environment

The property: non-interference

Two copies of a way-partitioned cache. The attacker gets the same ways and makes the same accesses in both; the victim may do anything.

copy 1
attacker + victim run A

copy 2
attacker + victim run B

Every attacker access hits in copy 1
⇔ it hits in copy 2, at every step

The environment: assumptions

The cache runs inside a system, so the inputs are constrained

assume (|attacker_hitmap);
if (choice == 2'b00) begin
  assume (hitmap1 == attacker_hitmap
        && hitmap2 == attacker_hitmap);
  ...
end

System property holds under the assumptions, but not for arbitrary inputs.

To mine the auxiliary invariants, we need to mine under assumptions

Cache designs from Godbole, Ye, Manerkar & Seshia, FMCAD 2023

44

Assumptions in the toolflow

DESIGN

+ assumptions

SIMULATE

traces of constrained inputs

NEGATIVE STATES

unreachable under the assumptions

COMPUTE mUS

variable sets

SYNTHESIZE ×k

conjecture includes the assumptions

VERIFY &

MINIMISE

final assertions

uses the assumptions

Assumption support added to each orange block

45

Auxiliary invariants

The end-to-end security property has complex data and timing dependencies, so it can’t be proved directly.

end-to-end property alone

not provable on its own

+ invariants written by experts

unbounded proof, after days of manual effort

+ invariants mined by MAPminer

the same unbounded proof: ~2 minutes of mining, 2 s to prove

MAPminer’s invariants are different from the experts’, but both make the same property provable.

46

Specification Mining

Hardware

Symbolic synthesis

SMART · MAPminer

Software

int check(int *a,
  int *b, int n) {
  ...
}

LLMs + verifiers

AutoC2VR

47

C to verifiable Rust

There’s a big push to migrate C to memory-safe Rust. C2VR [Xia et al. 2026] uses specifications to ensure correct translations:

C + ACSL

TRANSLATE & MIGRATE

LLM: C → Rust · rules: ACSL → Verus

Rust + Verus

VERUS

Needs existing ACSL specifications.

Needs manual repair when verification fails.

52.6% of programs verified automatically; 79.4% after manual fixes to code and proof annotations.

48

AutoC2VR

Executable C (no specs)

① SPECIFICATION SYNTHESIS

LLM proposes ACSL · Frama-C verifies · mutants refine

C + ACSL

② TRANSLATE & MIGRATE

C2VR: LLM translates C → Rust; rules migrate ACSL → Verus

Rust + Verus

③ VERIFIER-GUIDED PROOF REPAIR

LLM adds auxiiary invariants, never changes the code or the specs

Verified Rust + Verus

AutoC2VR (new)

C2VR

49

Specification synthesis

LLM PROPOSES

ACSL-annotated C

ADMISSIBLE?

code unchanged, no axioms

VERIFY

Frama-C

MUTANTS

how many does it kill?

inadmissible

unproved properties (+ counterexamples)

surviving mutants

Mutants used as feedback to the LLM

50

Example: comparing two arrays

int check(int *a, int *b, int n) {
  for (int i = 0; i < n; i++) {
    if (a[i] != b[i]) {
      return 0;
    }
  }
  return 1;
}

First verified spec: kills no mutants

ensures \result == 0 || \result == 1;

Surviving mutant, fed back to the LLM:

- if (a[i] != b[i]) {
+ if (a[i] <  b[i]) {

Refined spec: kills all the mutants

ensures \result == 0 || \result == 1;
ensures \result == 1 ==>
  (\forall integer k; 0 <= k < n ==> a[k] == b[k]);
ensures \result == 0 ==>
  (\exists integer k; 0 <= k < n && a[k] != b[k]);
loop invariant \forall integer k;
  0 <= k < i ==> a[k] == b[k];

51

Verifier-guided proof repair

The LLM may add

loop invariants
assertions
quantifier triggers
termination measures

…but must not

change the executable Rust
weaken the migrated pre/post conditions
add assumptions

fn mul(a: i32, b: i32) -> (result: i32)
  ...
  invariant
    // existing invariants unchanged
+   a > 0 ==> i32::MIN as int <= (a - x) * b,
+   a > 0 ==> (a - x) * b <= i32::MAX as int,
+   a > 0 ==> 0 <= x,

Three added loop invariants and Verus proves the translated function, with no changes to code or specs.

52

AutoC2VR: results

Spec synthesis

90.5%

of 210 C programs get specs that verify, generated from the code alone (original specs removed)

Spec quality: mutation score

+11.6 points

Mutation score = % of held-out mutants the specs catch. Ours catch 11.6 percentage points more than the original, human-written specs.

Proof repair

61.3%

of repair attempts on C2VR’s verification failures succeed, giving 19 more verified Rust translations

End to end, compared with C2VR

+14

more programs translated to verified Rust, with no specs supplied and no manual fixes

53

Specification Mining

Hardware

Symbolic synthesis

SMART · MAPminer

Software

int check(int *a,
  int *b, int n) {
  ...
}

LLMs + verifiers

AutoC2VR

Cyber-physical

Open questions

54

Can we mine for CPS?

I can collect data from simulations

Three simulated traffic scenes generated from one Scenic scenario

Three scenes generated from one Scenic scenario (Fremont et al., Scenic, PLDI 2019)

I can (probably) verify systems

?

How can I find meaningful unreachable states / bad states?

?

What does a mutation look like for a cyber-physical system?

55

// Dr. Elizabeth Polgreen · University of Edinburgh · elizabeth.polgreen@ed.ac.uk