Sekura JS Formal Verification: A First Step Toward Evidence for the Language

AI Summary: Assurance Sekura JS is building an inspectable evidence base for selected properties of programs compiled by Sekura JS. A requirement is connected to source code, a compiled .sobj object, an .sjv contract, and an .sjp proof package. The initial work covers selected arithmetic, control-flow, function, memory, and data-layout behaviors, while module and runtime ABI scenarios currently have test evidence rather than formal proofs. Programs are compiled at optimization levels O0–O4 and each resulting object is treated as a separate verification target. Restrictions such as n <= 3 keep some examples within the current verifier’s scope. This is partial progress, not a proof of the entire language or compiler: every result depends on its contract, assumptions, execution model, verifier, and supported constructs.

Can we prove that a compiled program does what it is supposed to do? For carefully stated properties of a particular program, formal methods can provide evidence. This is the starting point of Assurance Sekura JS: define explicit claims, connect them to concrete artifacts, and make the evidence available for inspection.

This is an initial, partial result. It does not prove the whole Sekura JS language or every program written in it. Its purpose is to establish a verifiable foundation and expand the scope incrementally, while making clear what has and has not been checked.

What Is Being Verified?

In Assurance Sekura JS, each verification claim connects a requirement, a source program, a formal specification, and a compiled artifact. The evidence chain is:

Requirement → source program → compiled object → contract verification → proof package.

Sekura JS source is compiled into a .sobj object. A separate .sjv specification defines the conditions under which the program is examined and the properties expected to hold after execution. The SJV verifier checks those properties against the compiled object and produces an .sjp proof package.

For example, a contract might require a function to return the sum of its arguments, a write to one structure field to preserve a neighboring field, or a local value to remain correct across a nested function call. These are claims about specific program behavior, not blanket guarantees about every use of the language.

Each claim has a defined scope: permitted inputs, environmental assumptions, observable effects, and known limitations. A result is meaningful only within those boundaries.

How This Differs from Testing

A test runs a program with selected inputs. A successful test confirms the observed behavior for those executions.

Formal verification can reason about every input permitted by a contract. Given symbolic arguments, the verifier searches for a violation across the contract’s specified input domain.

For an addition function, for example, the verifier can check that the result equals the sum of its arguments under the specified integer semantics. If the contract imposes no additional input restriction, that claim can cover all values of the relevant types supported by the model.

That does not establish correctness for every program that uses addition. The claim remains tied to one compiled object, one contract, and one verification model. Assurance Sekura JS makes this boundary explicit.

What the Initial Stage Covers

The current evidence is organized across five areas:

The selected programs are compiled at optimization levels O0–O4. Each resulting object is treated as a separate verification target, so evidence for one optimization level is not silently assumed to apply to another.

Test evidence remains distinct from formal evidence. A module scenario that completes successfully is useful information, but it does not become a formal proof simply because it ran without an error. The Sekura JS formal-verification overview describes the SJV contract and compiled-object verification flow in more detail.

Why Begin with Restricted Inputs?

Some early contracts deliberately define a narrow input domain. For example, arithmetic loop examples may be verified under the precondition n <= 3.

Within that precondition, verification considers every permitted input and feasible execution path represented by the current model. The restriction keeps the example within the capabilities of the symbolic execution mechanism while allowing the result to be complete within a clear boundary.

Future work can expand that boundary by weakening preconditions, adding scenarios, and extending verification methods. The restriction is not a claim that inputs outside the contract are safe; those inputs are simply outside the result’s scope.

Memory and call profiles follow the same principle. Some already check functional behavior, memory, address mapping, and stack preservation. Others establish only the returned value. Reporting those differences makes clear which questions have been answered and which remain open.

Partial coverage is expected at this stage. The value lies in stating each claim precisely and checking it against the stated scope.

Evidence Must Be Inspectable

Assurance Sekura JS preserves materials needed to examine results: source programs, specifications, compiled objects, proof packages, verification logs, and tool identities.

Hashes connect reports to exact files and tool binaries. Signatures support checks of package origin and integrity. Replaying stored SMT queries checks whether solver results can be reproduced.

These mechanisms answer different questions. A valid signature does not establish that a claim is true. Successful SMT replay does not remove the need to trust the verifier’s translation of program behavior into formulas. The execution model and verifier therefore remain part of the foundation for confidence in a result.

For the current limits of replay and source-to-proof provenance, see Proof Without Disclosing Source Code. The SJV language reference and SJP package format document the specification and evidence formats.

How the Verified Scope Can Grow

The next steps follow from the current profiles. Further work can cover missing operations and types, broaden permitted input states, and establish additional memory and call properties. It can then examine combinations of constructs: arithmetic inside loops, calls that modify memory, and interactions between modules.

These combinations matter because proving individual examples does not automatically prove arbitrary compositions. The evidence base must grow in breadth and depth. As it does, more general semantic arguments will be needed to explain how the verification models correspond to the language and machine execution, and under what conditions separate results can be composed.

The first stage of Assurance Sekura JS provides a concrete starting point. Claims, artifacts, and boundaries are available for inspection. Each extension can be assessed precisely: what additional behavior has been verified, which restrictions have been removed, and which questions remain open.

Explore the Assurance Sekura JS repository for the project and its verification evidence.