Proof Without Disclosing Source Code
Source code cannot always be shared with a customer, partner, auditor, or another organization. Trade secrets, licensing restrictions, security requirements, and intellectual-property protection may all require an implementation to remain private.
That does not necessarily mean that no meaningful evidence of correctness can be shared. The implementation and the evidence about its behavior are different things, provided the limits of that evidence are stated clearly.
In Sekura JS, three elements can be treated separately:
- Source code remains with its owner.
- An SJV contract describes the properties expected to hold.
- An SJP package carries results and mathematical obligations from a verification run.
SJV describes what should be proved. SJP carries evidence of the verification performed. The source code can remain private.
This model lets one party provide formalized behavioral requirements and a verification artifact without handing over the implementation itself. It does not, by itself, settle every question about whether the artifact came from the exact private source revision being claimed. That boundary is central to using the approach responsibly.
For the broader compiler-to-contract verification flow, see Sekura JS Formal Verification: Proving Compiled Programs Against SJV Contracts. The article below focuses on what can be exchanged when the source itself is not disclosed.
SJV as a Contract Between Parties
When a recipient cannot inspect the implementation, both parties need to agree in advance on what counts as correct behavior. An SJV contract provides a formal place to state that scope.
Depending on the supported language and verification environment, a contract can describe:
- permitted module states;
- conditions that must hold before a function is called;
- relationships between pre-state and post-state;
- invariants that must remain true;
- the environment and scope in which verification is performed.
The agreement is about observable, verifiable properties rather than the implementation’s internal design. A customer may not need to know how an algorithm is written. They may need evidence that a value remains within an allowed range, a forbidden state cannot be reached under stated assumptions, or an operation returns an allowed result for specified inputs.
Those claims need to be expressed in the contract and reviewed for relevance. A proof is only as broad as its contract and verification scope. If a requirement is absent from SJV, or falls outside the verifier’s supported model, a successful result says nothing about that requirement.
The SJV language reference describes the contract language, while the formal-verification overview explains how the verifier checks compiled Sekura JS programs against those contracts.
SJP as a Portable Proof Package
After an implementation has been checked against an SJV contract, the process can produce an SJP, or Sekura Justified Proof, package. SJP is intended to carry verification information separately from the source code.
Depending on the verification run and package configuration, an SJP may include:
- a verification manifest;
- information about inputs and configuration;
- recorded verification results;
- stored SMT obligations or queries;
- integrity-related data;
- a manifest signature, when signing is used.
The recipient can inspect the package without receiving the module’s source files. Stored SMT queries can be executed again with Z3; where the workflow calls for an additional cross-check, CVC5 may also be used.
Replaying those obligations gives the recipient more than an unsupported statement that “verification passed”: it provides concrete mathematical queries that can be checked independently. The SJP format documentation describes the package structure and the SJP signatures documentation covers its signature-related behavior.
However, replaying a stored query answers a specific question: whether that query is solved as reported under the replay environment. It does not automatically establish where the query came from or whether it faithfully represents the implementation the sender identifies.
What an SJP Signature Does—and Does Not—Prove
An SJP manifest can be signed with Ed25519. A recipient can then check whether the manifest matches a signature made for a particular public key and whether the signed content has been altered.
That check must not be confused with identifying or trusting the key owner.
A signature can answer:
Does this manifest match a signature for this public key?
By itself, it cannot answer:
Who controls this key, and should that party be trusted?
Sekura JS does not turn a cryptographic key into an identity certificate. The parties must establish trust in the public key separately, for example through an existing organizational agreement, corporate key infrastructure, an audit procedure, or another mechanism they accept.
A Practical Exchange Between Organizations
A source-private verification exchange can be organized as a sequence of explicit decisions:
- The developer and recipient agree on the behaviors and risks that need to be addressed.
- Those properties and assumptions are expressed in an SJV contract.
- The developer verifies a particular implementation against that contract using a defined toolchain and environment.
- The verification process produces an SJP package containing the applicable results and obligations.
- The developer transfers the SJV contract and SJP package without transferring the source code.
- The recipient reviews whether the contract actually covers the requirements that matter.
- The recipient checks the package and re-executes its stored SMT obligations.
- If the package is signed, the recipient verifies the signature and separately establishes whether the signing key is trusted.
This gives the recipient two distinct kinds of information: what behavior was required and which mathematical obligations were reported as checked. The source can remain inside the developer’s organization, while the contract, package, and verification procedure are made available for review.
For teams managing verification records alongside requirements, implementation revisions, and other engineering evidence, Sekura Noda Assurance describes a separate evidence-management layer. Noda organizes evidence and traceability; it does not itself run the verifier or establish that a proof is valid.
Separate the Claims Being Made
Several claims are involved in this exchange. They should be evaluated independently rather than compressed into a single statement that a system is “verified.”
Contract scope
SJV defines which properties are being checked, along with relevant assumptions and scope. A property omitted from the contract is not established by an SJP result.
Mathematical obligations
The SJP contains obligations produced or recorded by a verification process. Replaying the stored SMT queries checks whether those obligations are solved as reported in the replay environment.
Package integrity
Structural validation and integrity mechanisms can detect malformed or modified package contents, subject to the guarantees of the mechanisms used.
Signature and key trust
An Ed25519 signature can bind a manifest to a private key. Establishing the identity and trustworthiness of the key owner requires a separate trust process.
Binding to the implementation
There is a further question:
Were the obligations in this SJP actually derived from the exact version of the private source code that the developer claims was verified?
This is not the same as replaying the SMT queries. A recipient may successfully replay every stored query while still lacking independent evidence that those queries were generated from the claimed source revision.
The Current Boundary: Replay Is Not Source-to-Proof Provenance
In the current implementation, verify-sjp checks package structure and integrity, verifies a signature when one is present, and re-runs the SMT queries stored in the SJP.
It does not receive the closed source code and regenerate the proof obligations from that source code.
Therefore, a successful verify-sjp run supports these claims:
- the transferred package passed the applicable structure and integrity checks;
- the signature matches the specified public key, if the package is signed;
- the stored SMT obligations can be replayed with the reported results in the verification environment.
By itself, it does not prove that the stored obligations were correctly generated from the exact private source revision identified by the sender. This is the principal boundary of the “proof without source disclosure” model, and it should be disclosed to recipients rather than left implicit.
Establishing Confidence in Proof Provenance
If replaying the SJP is not enough, and the recipient also needs confidence in the origin of the proof, the exchange needs an additional process for establishing the chain:
source revision → proof generation → SJP
The right process depends on the risk model and agreement between the parties. Options may include:
- an independent auditor inspecting the source and proof-generation process;
- generating the SJP in a controlled, reviewable environment;
- disclosing source code only to a trusted third party;
- recording the exact source revision, toolchain, configuration, and proof-generation procedure;
- another agreed mechanism that provides evidence connecting the implementation to the obligations in the package.
These mechanisms create an organizational and technical trust model on top of the proof format. An SJP should make its own boundary visible: package verification is not automatically proof provenance.
Why the Middle Ground Is Useful
Without a way to share structured evidence, organizations can face an unnecessarily binary choice: disclose the complete source code or ask the other party to trust an internal statement that verification passed.
SJV and SJP provide a middle ground. A developer can keep the implementation private while sharing:
- a formal description of the properties under review;
- a portable verification package;
- the mathematical obligations recorded in that package;
- a way to replay those obligations independently;
- cryptographic protection for package contents when signing is used.
The recipient can assess whether the contract is meaningful and whether the transferred proof artifacts behave as reported. The parties can then decide whether their risk model also requires a separate source-to-proof provenance process.
Not a “Proof of Everything”
An SJP does not mean:
“This module contains no defects.”
It supports a narrower and more useful statement:
For a defined verification scope, specific mathematical obligations were recorded, and the transferred package allows the reported results of those obligations to be checked again.
The strength of that statement depends on at least three factors:
- How completely the SJV contract reflects the requirements that matter.
- How correctly the proof obligations are generated from the implementation.
- How reliably the recipient can establish the relationship between the verified implementation and the SJP being reviewed.
Those factors should be documented separately. Doing so makes the evidence easier to evaluate and prevents a technically valid replay from being presented as a broader guarantee than it supports.
Proof Can Travel Separately From the Implementation
Formal verification does not always require source code to be disclosed to every participant. SJV gives the parties a way to define the properties a system is expected to satisfy. SJP gives them a way to transfer and replay evidence of specified mathematical checks. The source code can remain with its owner.
The distinction must remain precise: an SJP can provide verifiable evidence about stored mathematical obligations, while confidence in a closed implementation also depends on how the relationship between that implementation and the obligations is established.
By keeping contract scope, proof replay, package integrity, signature trust, and proof provenance separate, organizations can discuss verification of closed systems without claiming more than the proof artifact itself demonstrates.