Sekura JS: Formal Verification of Compiled Programs Against SJV Contracts

AI Summary: Sekura JS can now formally verify a compiled program against an SJV contract. The verifier analyzes the actual SOBJ artifact, builds a symbolic execution model, and uses the Z3 SMT solver to search for a possible violation. A SAT result returns a concrete counterexample; an UNSAT result means that no violating execution was found within the declared contract, environment, execution model, and supported verifier capabilities. Successful verification produces an SJP report that records the source, contract, compiled artifact, and verification environment. This is stronger than ordinary testing, but it is not an unlimited proof: current scope is constrained by supported operations, environments, loops, optimization behavior, and dynamic MMU state.

Sekura JS can now not only compile systems code, but also formally verify the compiled program against a specification.

The verification is not limited to a handful of test cases and does not stop at the source-code level. The system analyzes the actual compiled SOBJ artifact, builds a symbolic model of its execution, and uses the Z3 SMT solver to search for any possible violation of the contract.

If such a violation exists, the system returns a concrete counterexample.

If Z3 proves that no counterexample exists, the implementation is considered formally verified within the scope of the contract, environment, execution model, and supported verification capabilities.

From Source Code to Proof

The complete pipeline is:

Sekura JS source
      ↓
     .sjs
      ↓
  compiler
      ↓
     .sobj
      +
     .sjv
      +
 environment
      ↓
symbolic execution
      ↓
proof obligation
      ↓
      Z3
   ↙      ↘
 SAT      UNSAT
  ↓         ↓
error     proved

After successful verification, the system generates an .sjp report: a Sekura Justified Proof report tying the result to exact versions of the source code, specification, compiled artifact, and verification environment.

What Is SJV?

.sjv is the formal specification language of the Sekura Justified System.

It does not describe how a function must be implemented. It describes what state is allowed before a call, what inputs are valid, and what must be true after the function returns.

For example:

let counter: u32;

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

Its contract can be written as:

module counter.sjs;

function increment {
    counter' = counter + 1;
}

Here counter means the value before the call, while counter' means the value after the function has completely returned. The expression counter' = counter + 1 is a mathematical requirement, not an assignment command.

Verification Happens at Function Boundaries

SJV is centered around the function boundary:

state before call
       ↓
    function
       ↓
state after return

The contract does not need to hold after every internal instruction. A function may use temporary values, reorder calculations, or transform its internal representation. What matters is that every final observable state satisfies the contract.

The internal execution is still analyzed. It must be analyzed to determine possible final states and to detect invalid operations during execution.

State, Preconditions, and Conditional Results

SJV can define valid module states. Expressions in one state block are combined with logical AND:

module motor.sjs;

{
    motor.speed < 100;
    motor.enabled <= 1;
}

Several blocks can describe alternative valid states. The module is valid when at least one block is satisfied.

An expression inside function that does not contain ' defines a condition for an allowed call:

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

This contract requires the precondition before the call and the postcondition after return. The verifier is not required to prove behavior for inputs outside the declared contract.

Conditional postconditions are also explicit:

function update {
    enabled != 0 => {
        counter' = counter + 1;
    }

    enabled == 0 => {
        counter' = counter;
    }

    enabled' = enabled;
}

SJV has no hidden rule that an unmentioned field must remain unchanged. If a property matters, the contract must state it.

The Formal Model

At a high level, the verifier constructs a formula describing:

valid initial state
∧ valid function inputs
∧ possible execution of the compiled program
∧ violation of the required postcondition

The question given to Z3 is deliberately the question of failure:

Does there exist an allowed execution that violates the contract?

If the answer is SAT, the formula has a satisfying assignment. That assignment is a counterexample: concrete initial values and inputs that lead to a contract violation.

If the answer is UNSAT, no such violating execution exists within the encoded model. The implementation is therefore proved against that contract within the declared scope.

Verifying the Specification Itself

The contract is part of the verification input, so it must be checked as well.

The verifier validates that referenced variables and functions exist, expressions are well-formed, types are compatible, preconditions and postconditions use the supported semantics, and the specification can be translated into the symbolic model.

This prevents a successful result from being attributed to a contract that was silently ignored, misunderstood, or only partially translated.

Verifying the Implementation

The verifier does not simply re-evaluate the source-level expression.

It loads the compiled .sobj artifact and symbolically executes the instructions supported by the verification engine. Registers, local frames, memory values, control flow, and relevant environment state become symbolic values or symbolic constraints.

This distinction matters. A source-level proof can miss a compiler transformation error. Verification of the SOBJ artifact checks the representation that will actually be consumed by the runtime.

The intended chain is:

source semantics
      ↓
compiler output
      ↓
symbolic execution of SOBJ
      ↓
SJV postcondition

Verification by Searching for a Counterexample

The verifier’s central strategy is practical and precise: ask whether a bad execution is possible.

For example, if a function should increment a counter, the verifier searches for a permitted initial state in which the compiled instructions return with a value other than the required result.

When Z3 returns SAT, the result is not merely “failed.” It contains a model that can be rendered as a diagnostic counterexample. That makes the failure useful for debugging the contract, the compiler, or the program.

When Z3 returns UNSAT, the verifier has eliminated all violating executions represented by the model. It has not merely observed that selected examples passed.

Why This Is Not Ordinary Testing

Tests sample executions.

Formal verification searches a symbolic space of executions.

A test might run a function with counter = 0, counter = 1, and counter = 100. A contract verifier can reason about the complete range represented by the chosen integer semantics and environment, subject to the limits of the model.

Testing remains important. It exercises integration, performance, unsupported environments, and behavior outside formal scope. Formal verification adds another layer: it can prove that no modeled counterexample exists, or produce one that ordinary tests did not happen to include.

The two approaches should reinforce one another rather than compete.

Machine Arithmetic Is Part of the Model

The verifier models machine values, not unrestricted mathematical integers.

Bit width, signedness, wrapping behavior, comparisons, shifts, and conversions must be represented explicitly. A proof about unbounded integers would not automatically be a proof about the generated machine-level behavior.

This is one reason verification belongs close to the compiled artifact and the target execution model. The relevant question is not only whether an equation is mathematically elegant, but whether it remains true under the arithmetic semantics of the processor and runtime.

A Real Compiler Bug Found During Verification

One of the strongest reasons to verify compiled artifacts is that the process can find errors in the compiler itself.

A source program can be correct, and its SJV contract can be correct, while the generated code still implements the wrong operation. A source-level check may never expose that mismatch.

When symbolic execution of the SOBJ artifact finds a counterexample, the investigation can compare the contract, source behavior, intermediate artifacts, generated instructions, and final machine state.

In this workflow, a counterexample is not only a failure report. It is an executable explanation of how an implementation diverges from its declared behavior.

Once fixed, the counterexample can become a regression test, preventing the same compiler defect from returning later.

Verification Identity and SJP Reports

The result must be tied to what was actually verified.

An SJP report records the identity of the source, SJV contract, SOBJ artifact, compiler, target configuration, environment, and verifier capabilities. This prevents a generic “verified” label from becoming detached from the exact inputs that produced it.

The current SJP format is a verification report, not an independent proof certificate. It documents the result and its identity, but the report itself is not yet a self-contained proof object that another implementation can independently replay without the original verification machinery.

That distinction is important for precise communication.

What Does VERIFIED Mean?

VERIFIED does not mean that every possible property of a program has been proved.

It means that, for the selected function or module, contract, machine arithmetic, environment, execution model, and supported instruction set, the verifier found no counterexample to the specified obligations.

Verification result levels can therefore distinguish successful proof, a discovered counterexample, an unsupported construct, an invalid specification, and an inconclusive or resource-limited analysis.

Current Limitations

The current verifier has a defined scope.

Dynamic MMU behavior, unsupported operations, complex environments, optimization-sensitive transformations, and loops may require additional modeling or bounded treatment. A result outside that scope must not be presented as a proof of the complete system.

Loops are especially significant. An unbounded loop requires an invariant or another method of representing all relevant iterations. Running a fixed number of iterations can be useful for testing, but it is not automatically a proof of the unbounded behavior.

The same discipline applies to memory and operating-system behavior. If the environment is abstracted, the result applies to that abstraction. If a feature is unsupported, the verifier should report that limitation rather than silently treating the operation as verified.

Why This Matters for Systems Programming

Systems software sits at the boundary between source-level intent and machine-level behavior.

The compiler changes representation. The runtime supplies an environment. The operating system manages resources. The processor applies architectural rules. Bugs can arise at every boundary.

SJV gives the program a declared behavioral contract. SOBJ verification checks the compiled representation. Z3 searches for counterexamples. SJP records what was checked.

Together, these mechanisms create a path toward a more inspectable systems stack:

Sekura JS source
      ↓
SJV contract
      ↓
compiler
      ↓
SOBJ artifact
      ↓
symbolic execution
      ↓
Z3
      ↓
SJP verification report

SJS and SJV

Sekura JS and SJV have complementary roles.

Sekura JS describes how a program is written and compiled. SJV describes the behavior that must be preserved at a function or module boundary.

This separation allows implementation and specification to evolve independently while remaining connected by a formal obligation. A developer can change the internal algorithm without changing the contract, provided the compiled result still satisfies it.

The specification can also come before the implementation. Writing the expected state transition first makes the intended behavior explicit and gives the compiler and verifier a target that can be checked continuously.

Current Status and Next Directions

The current system demonstrates the core loop:

write SJV contract
        ↓
compile Sekura JS
        ↓
load SOBJ
        ↓
symbolically execute
        ↓
ask Z3 for a counterexample
        ↓
produce SAT diagnostics or UNSAT result
        ↓
write SJP report

The next directions are to expand instruction coverage, improve counterexample presentation, strengthen verification identity, support more realistic environments, handle loops with explicit invariants, and make the result easier to reproduce independently.

The long-term objective is not to attach a “formal” label to every program automatically. It is to make the boundary between intended behavior and compiled execution precise enough that failures can be found, explained, fixed, and prevented.

The Core Idea

The essential idea is simple:

do not trust only the source
do not trust only the tests
do not trust only the compiler

state the contract
compile the program
analyze the artifact
search for a counterexample
record exactly what was verified

Sekura JS formal verification is a step toward a computing stack in which source code, compiler output, runtime behavior, and processor execution can be connected by explicit, testable, and increasingly machine-checkable contracts.