I Built Formal Verification for Compiled Sekura JS Programs with SJV and Z3

The Gap Between Source and Binary

Most developers trust this pipeline:

source code ↓ compiler ↓ binary

If the source looks correct and the tests pass, we usually assume the compiled program behaves correctly too. But there is still a gap:

correct source code ↓ compiler bug ↓ incorrect machine code

I wanted to close that gap in Sekura JS. The result is now a working verification pipeline:

SJS ↓ compile ↓ SOBJ ↓ symbolic execution ↓ SJV proof obligation ↓ Z3 ↓ SAT / UNSAT

The important part is this: The verifier checks the compiled SOBJ implementation, not only the Sekura JS source code.

The Basic Idea

Sekura JS is a systems programming language. SJV is its formal specification layer. An .sjs file describes the implementation. An .sjv file describes what the implementation must guarantee.

For example:

let counter: u32;
let increment(): void {
    counter = counter + 1;
}

The SJV contract is:

module counter.sjs;
function increment {
    counter' = counter + 1;
}

The syntax is intentionally small. Here: counter means the value before the function call. And: counter' means the value after the function returns. So: counter' = counter + 1 is not an assignment. It is a mathematical statement about the required result.

What Exactly Is Being Proved?

Let:

• S be the state before the function.
• S' be the state after it returns.

Then define:

• I(S) as the allowed module state.
• P(S, input) as the function precondition.
• T(S, input, S') as the required result.
• E(S, input, S') as the actual execution relation of the compiled implementation.

The property we want is:

∀ S, input, S': I(S) ∧ P(S,input) ∧ E(S,input,S') → T(S,input,S') ∧ I(S')

In plain English: For every allowed initial state and every allowed input, every possible completion of the compiled function must satisfy the SJV contract and leave the system in an allowed state.

We Prove It by Searching for a Bug

Instead of proving the implication directly, the verifier asks Z3 to find a counterexample:

∃ S, input, S': I(S) ∧ P(S,input) ∧ E(S,input,S') ∧ ¬( T(S,input,S') ∧ I(S') )

That means: Can there exist any valid state and input for which the compiled implementation violates the contract?

Now Z3 gives us three useful outcomes:

• SAT - a counterexample exists.
• UNSAT - no counterexample exists within the verification model.
• UNKNOWN - the solver could not prove or disprove the property.

For a successful proof, we need: UNSAT.

A Tiny Example

Suppose the contract is:

function increment {
    counter' = counter + 1;
}

And the implementation really does:

counter = counter + 1;

The verifier builds the symbolic execution model and asks Z3 whether this can ever violate the contract. If Z3 returns: UNSAT, the implementation satisfies the contract for all allowed values in the verified domain.

Now change one line:

counter = counter + 2;

The specification stays the same. The solver can now return: SAT with a concrete counterexample. For example:

• counter before = 0
• expected: counter after = 1
• actual: counter after = 2

This is the part I find most useful in practice. The verifier does not only say: verification failed. It can tell you which state makes it fail.

This Is Different from Testing

A normal test may check:

counter = 10
increment()
counter == 11

That proves one example. Formal verification considers: counter = any allowed u32 and checks the property across the whole verified state space. That distinction matters.

TEST PASSED does not mean: VERIFIED

Both are useful, but they answer different questions.

Why Verify the Compiled Artifact?

This was one of the core design choices. If I verified only SJS source code, the compiler would remain outside the proof boundary. The real pipeline would still be:

verified source ↓ compiler ↓ unverified machine code

So the verifier works against SOBJ, the compiled Sekura JS object. Conceptually:

SJV specification + compiled SOBJ ↓ symbolic execution ↓ proof obligation ↓ Z3

That also turned out to be useful for finding compiler bugs.

Formal Verification Found a Real Compiler Bug

During implementation, the verifier exposed a bug in the Sekura JS compiler. A global: u32 value was incorrectly treated as a pointer. Because of that, ordinary arithmetic could be scaled as pointer arithmetic. An addition that should have behaved like:

value + 1

could effectively be treated as if the increment had to be multiplied by the element size. The bug was fixed. This is exactly why verifying the final compiled representation is valuable. The verifier is checking what the compiler actually produced, not what we hoped it produced.

SJV Contracts Can Describe State Transitions

The contracts are not limited to simple return values. For example:

struct Counter {
    value: u32;
    limit: u32;
};

We can define an allowed state:

{ counter.value <= counter.limit; }

and a function contract:

function increment {
    counter.value < counter.limit => {
        counter.value' = counter.value + 1;
    }
    counter.value == counter.limit => {
        counter.value' = counter.value;
    }
    counter.limit' = counter.limit;
}

This says: if the counter is below the limit, increment it; if it has reached the limit, leave it unchanged; the limit itself must not change.

Notice the last line: counter.limit' = counter.limit;. SJV does not assume that unspecified fields remain unchanged. If preserving a value matters, it must be part of the contract.

Function Boundaries Are the Verification Boundary

SJV describes:

state before call ↓ function ↓ state after return

It does not require the contract to be true after every internal operation. A function may temporarily use intermediate values that do not satisfy the final contract. The symbolic executor still analyzes the internal execution to determine possible results and detect invalid operations. But the functional specification is about the final state of the function.

I deliberately kept this model simple because it maps naturally to normal systems programming.

Machine Arithmetic Matters

The verifier cannot silently use mathematical integers where the language uses machine integers. For example:

let x: u32 = 0xffffffff;
let y: u32 = x + 1;

must produce:

y = 0

The verification model therefore uses the actual 32-bit modular semantics of Sekura JS. The same principle applies to: u8, i8, u16, i16, u32, i32, including storage width, extension on load, and truncation on store.

What Is Currently Checked?

The current implementation includes verification for:

• SJV contracts
• memory bounds
• memory alignment
• static MMU behavior
• stack constraints
• ABI preservation
• initial environment registers
• symbolic memory behavior
• overlapping memory accesses

The system also tracks the current verification stage, function, and elapsed time. When verification fails, diagnostics can include:

• function
• SJV contract location
• input values
• register values

Register values are shown in hexadecimal form.

A Larger Verification Scenario

The small identity example is useful, but I also wanted something closer to a real stateful system. The current verification_workflow example contains:

• 6 states
• 10 functions
• global variables
• state transitions
• counter arithmetic

The correct implementation verifies successfully. If I introduce an intentional bug in the add function, the verifier rejects it. That gives much more confidence than a verifier that only works on: x = x + 1 examples.

Current Test Status

The latest complete project run is:

41 / 41 tests passed

The VS Code extension also supports: .sjs, .sjv, .sasm, .smod, .sdef, .sjp with:

7 / 7 syntax-highlighting tests passed

What Is SJP?

After successful verification, the tool generates an .sjp artifact. It records information such as:

• source hash
• SJV hash
• SOBJ hash
• verifier version
• verification scope
• results
• assumptions
• dependencies

The goal is to bind a verification result to exact inputs. But there is an important limitation. Today, SJP is a verification report / proof artifact. It is not yet an independently checkable proof certificate. A separate tiny checker cannot currently validate the entire proof without rerunning the verifier. That is a possible future direction.

What Does VERIFIED Actually Mean?

This is worth stating carefully. VERIFIED does not mean:

This program can never have any bug in any possible environment.

It means:

The implementation satisfies the given SJV specification for all allowed states and inputs within the declared environment, execution model, and supported verification scope.

That qualification is important. Formal verification is only as strong as:

• the specification
• the execution model
• the assumptions
• the supported verification scope

If a requirement is missing from SJV, it has not magically been proved.

Current Limitations

The current verifier still has boundaries.

Optimization

The current example environment is tied to: -O0. Optimizations can change addresses, remove functions, and restructure the compiled program. Supporting optimized builds requires the state mapping and verification environment to account for those changes.

Dynamic MMU

Static MMU verification is supported. Dynamic MMU behavior still needs more work.

Unsupported Operations

If the symbolic executor cannot model an operation correctly, the path must not be silently considered proved. The result should remain: UNSUPPORTED or: INCONCLUSIVE.

Loops

Bounded unrolling is not a proof of an arbitrary loop. Loops that cannot yet be closed by the verification model remain an area for further work.

Where the Project Stands Now

As of September 8, 2026, the working pipeline is:

SJS ↓ SOBJ ↓ symbolic execution ↓ SJV proof obligation ↓ Z3 ↓ SAT / UNSAT ↓ SJP

The current implementation is committed to the main repository at: 8a2aca8. Generated artifacts are not stored in the commit.

What I Like About This Model

The most useful change is not Z3 itself. It is the development mindset. Instead of only asking:

How should I implement this function?

I can first ask:

What exactly must this function guarantee?

For example:

• before: balance = B, amount <= B
• operation: withdraw(amount)
• after: balance = B - amount

Then write:

function withdraw {
    amount <= account.balance;
    account.balance' = account.balance - amount;
}

Then implement the function. Then compile it. Then verify the actual compiled program. That gives a workflow like:

specify ↓ implement ↓ compile ↓ verify ↓ counterexample ↓ fix

And if a counterexample exposes a real bug, it can become a normal regression test.

Final Thought

Systems programming usually forces us to be explicit about memory, integers, addresses, layouts, and state. Formal verification should be equally explicit about correctness. That is the direction behind Sekura JS + SJV: implementation + formal specification + compiled artifact + symbolic execution + SMT proof.

The goal is not to replace testing. The goal is to add a stronger question:

Can any allowed execution of this compiled function violate the contract?

If Z3 answers: SAT, we get a bug. If it answers: UNSAT, we have proved that no such counterexample exists within the verification scope. That is the foundation of the Sekura Justified System.