Sekura JS Formal Verification: Proving Compiled Programs Against SJV Contracts
Sekura JS now verifies the compiled SOBJ artifact against formal SJV contracts. This article explains the source-to-proof pipeline, preconditions, postconditions, symbolic execution, SAT and UNSAT results, counterexample diagnostics, verification identity, and the limits of the current system.