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

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. Let: 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, and: 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 means a counterexample exists. UNSAT means no counterexample exists within the verification model. UNKNOWN means 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.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