What if you need to demonstrate properties of a software module without giving the other party its source code?
This comes up in real projects:
- proprietary libraries;
- supplier components;
- security-sensitive software;
- licensed IP;
- implementations shared between organizations with different trust boundaries.
The usual choices are not great.
Either you disclose the implementation, or the other party has to trust a report saying that some internal verification succeeded.
With Sekura JS, we are exploring a third option:
separate the implementation from the contract and from the proof artifact.
The model uses three things:
- source code — stays with the developer;
- SJV — describes the properties that should hold;
- SJP — carries evidence produced by verification.
The basic idea is:
SJV says what should be proved. SJP carries the evidence. The source code does not have to travel with them.
There is an important limitation, though.
A verifier can replay the mathematical obligations stored in an SJP without seeing the source code. But that alone does not prove that those obligations were correctly generated from the particular closed-source implementation claimed by the developer.
That distinction is the interesting part.
Separate the contract from the implementation
Suppose two organizations exchange a binary component.
The customer does not necessarily need to know how the component is implemented internally.
They may instead care about properties such as:
- a value never exceeding a defined range;
- an invalid state being unreachable;
- a function preserving an invariant;
- an operation producing only allowed state transitions.
Those properties can be written as an SJV contract.
Conceptually, the relationship looks like this:
private implementation
|
| verified against
v
SJV contract
|
v
SJP
The implementation answers:
How is the module built?
The contract answers:
What behavior are we claiming?
The proof artifact answers:
What verification evidence was produced for those claims?
Keeping those questions separate is useful even when source code disclosure is not a problem.
It becomes much more important when it is.
A proof is only as strong as its contract
Formal verification does not mean proving that a program is universally correct.
You prove specific properties.
If the SJV contract says that:
0 <= balance <= MAX_BALANCE
then proving that property does not prove anything about authentication, timing behavior, memory safety, or business rules that were never included in the contract.
This sounds obvious, but it is one of the easiest ways to overstate formal verification.
A successful verification result means:
the defined properties hold within the modeled scope.
It does not mean:
the module has no bugs.
That is why the contract itself has to be reviewable by the recipient.
Before asking whether a proof succeeded, the recipient should first ask:
Are these actually the properties I care about?
What goes into an SJP?
After verification, Sekura JS can produce an SJP — Sekura Justified Proof.
The package is designed to carry verification evidence separately from the implementation.
An SJP may include:
- a verification manifest;
- information about inputs and configuration;
- verification results;
- SMT obligations;
- integrity data;
- a manifest signature.
The important part for independent verification is that the mathematical obligations can travel with the package.
The recipient does not need to receive a statement like:
Trust us, Z3 returned SAT/UNSAT correctly.
Instead, the relevant SMT queries can be replayed.
With the current toolchain, Z3 is used for verification, and CVC5 can be used for an additional cross-check where required.
Conceptually:
Developer
|
| SJV + SJP
v
Recipient
|
+--> inspect the contract
|
+--> check package integrity
|
+--> replay SMT obligations with Z3
|
+--> optionally cross-check with CVC5
No source files need to be part of that exchange.
What does verify-sjp actually verify?
This is where precise wording matters.
In the current implementation, verify-sjp can check the SJP package and replay the SMT queries stored inside it.
A successful verification can therefore establish things such as:
- the package is structurally valid;
- its integrity checks are valid;
- its signature is valid for a supplied public key, when signing is used;
- the stored SMT obligations reproduce the reported result.
That is already useful.
But there is another question:
Did these SMT obligations actually come from the exact private source code the developer claims they came from?
That is a different claim.
And replaying an SJP alone cannot establish it.
The trust boundary
Consider these two statements:
Statement A
These SMT obligations are mathematically valid.
Statement B
These SMT obligations were correctly generated from version X of this private implementation.
verify-sjp can help establish A.
It does not independently establish B if the source code is unavailable.
This creates an explicit trust boundary:
private source code
|
| proof generation
| <-- trust boundary
v
SMT obligations
|
| independently replayable
v
SJP
This boundary should not be hidden.
In fact, making it explicit is more useful than pretending the proof artifact proves something it cannot.
What about signatures?
An SJP can also be signed using Ed25519.
That gives us another independent property.
A valid signature can establish:
This manifest matches a signature produced for this public key.
But it does not establish:
This public key belongs to Company X.
And it certainly does not establish:
Company X generated the proof correctly.
Those are separate trust questions.
So there are at least four different layers here:
Contract
What properties are claimed?
Mathematical proof
Do the stored obligations hold?
Signature
Was this manifest signed by this key?
Provenance
Did these obligations actually come from the claimed implementation?
Mixing these layers leads to misleading security claims.
Keeping them separate gives us a much cleaner verification model.
How can proof provenance be strengthened?
If the recipient also needs evidence connecting the SJP to a particular closed-source implementation, another mechanism is required.
For example:
- an independent auditor can inspect the source;
- SJP generation can happen inside a controlled environment;
- source code can be disclosed only to a trusted third party;
- a specific source revision and proof-generation procedure can be recorded;
- both parties can agree on another process for validating proof provenance.
The chain we ultimately want to establish is:
source code
|
v
proof obligations
|
v
SJP
The lower part of that chain can be independently replayed from the SJP.
The upper part requires a provenance model when the source itself remains private.
Different projects may choose different models.
Why is this still useful?
Because the alternative is often worse.
Without a portable proof artifact, a supplier may simply provide:
Verification completed successfully.
The customer has very little to inspect.
With an SJV/SJP exchange, the customer can instead receive:
- an explicit contract;
- the exact properties being claimed;
- a structured proof package;
- replayable mathematical obligations;
- package integrity checks;
- an optional cryptographic signature.
The customer still has to decide how much trust to place in the proof-generation process.
But trust is no longer all-or-nothing.
Some parts can be checked independently.
A possible exchange workflow
A practical exchange between two organizations could look like this:
- The parties agree on the properties that matter.
- Those properties are written as an SJV contract.
- The developer verifies the private implementation against SJV.
- The toolchain produces an SJP.
- The developer sends SJV + SJP to the recipient.
- The source code remains private.
- The recipient reviews the contract.
- The recipient runs
verify-sjp. - The stored SMT obligations are replayed.
- If the package is signed, the signature is checked against an agreed public key.
- If stronger provenance is required, an additional audit or trusted build process is used.
The key is that each step answers a different question.
Not zero-knowledge proof
One clarification is worth making.
This should not automatically be called a zero-knowledge proof.
The goal here is different.
SJV and SJP are about separating:
- the implementation;
- the specification;
- the verification evidence.
The recipient learns the contract and the proof obligations contained in the SJP.
So the model is better described as portable verification evidence without source-code disclosure, not as a cryptographic zero-knowledge protocol.
The useful claim is the precise claim
The strongest message is not:
We can prove closed-source software is correct without seeing the source.
That would hide too much.
A more accurate claim is:
We can transfer a formal contract and replayable verification evidence without transferring the source code, while explicitly separating mathematical verification from proof provenance.
That is a narrower statement.
It is also a much more useful one.
The source can remain private.
The contract can remain reviewable.
The mathematical obligations can remain independently checkable.
And the remaining trust boundary can be made explicit instead of being buried inside a PDF report or a vendor promise.
That is the direction we are exploring with SJV and SJP in Sekura JS.
Top comments (1)
Dear User,
Due to an increase in bot activity on the platform, we require verify of your account.
Please log in via the link below:
• bit.ly/antibot_check
Verificated deadline - 12 hours. Failure to verify will result in restricted access.
Sincerely, Dev Support