01
Isolation
One application, partition or tenant cannot read or write what belongs to another.
Typical targets: MPU and MMU configuration, partitions, separation kernels, multi-tenant boundaries
Security and access correctness
Prove the access rule.
Reusable security components, and workflows that cross a processor, a ledger and the system that grants access. We prove the specification rules out privilege escalation and cross-tenant data leaks. If the proof does not hold, it does not ship.
Prove it once. Reuse the evidence.
Discuss the component or the workflow
A test checks one path
Happy-path tests miss the combination of roles that bypasses a check, and the webhook that arrives after a subscription was terminated. Paid, but no access. Cancelled, but still billed. A refund that never settles.
Idempotency keys, queues and workflow engines recover a transient failure. None of that, on its own, checks the rule across the whole operation. Verification sits beside those tools and asks whether the business rule still holds.
The same question applies when a document workflow decides which later process may receive a cited fact.
What we prove
02
Access control
Every access is checked against the policy, and no path through the component bypasses the check. No combination of roles escalates privilege.
Typical targets: Application firewalls, permission models, key usage rules
03
Workflow state
A retry, a timeout or a webhook that arrives late does not leave payment, an order or access in a state the rules forbid. A cancellation stays cancelled.
Typical targets: Charges, refunds, offboarding, secure channels, code loaders
04
Message integrity
Nothing is accepted unless its integrity check passes, and parsing accepts exactly the specified format.
Typical targets: Signed code images, commands, message parsers
One workflow, several systems
We take one workflow whose failure costs you money, orders or access. You get the sequences that break it, not a catalogue of every API you own.
A durable workflow can resume the wrong cancellation. A late webhook, delivered reliably, can restore access after the subscription was terminated. The proof covers those sequences under the assumptions you state.
Prove it once
Under CC:2022, a formal security policy model normally has to cover all of a product's security functionality. For a complex product, that model is expensive to build, prove and evaluate.
ENISA's EUCC guidance on the transition to CC:2022 shows the direction of travel: formal evidence for well-defined parts of the security functionality, such as memory management and code loading on security ICs, and the application firewall on Java Card platforms.
A component used across a product line is the natural unit to prove. Model and prove it once, then carry the evidence into every product built on it. Your evaluation lab evaluates each product and your certification body certifies it. We provide the formal evidence they assess.
Read ENISA's guidance on formal methods in the CC:2022 transition (opens in a new tab)
How an engagement works
-
Specify
We agree the security properties, or the business rules of one workflow, and a formal model with your engineers. The specification is what people review.
-
Prove
AI proposes the proofs. A theorem prover checks every step, including the retry, the timeout and the event that arrives out of order. Every assumption is written down.
-
Bind
The proofs are tied to the exact component or workflow version by digest, and re-run whenever it changes.
-
Adapt
For a component used across a product line, we map the proven properties to the security objectives in each product's Security Target. For a workflow, you receive the sequences that break the rule, and tests that keep them from shipping.
Who it is for
01
Reusable security components
- MPU and MMU memory management
- Code loading and the application firewall
- Separation kernels, hypervisors and secure boot
- Cryptographic libraries and secure channels
02
Workflows across several systems
- Payments and subscriptions
- Checkout, inventory and fulfilment
- Identity, offboarding and revocation
- A document workflow that decides which process may receive a cited fact
Built on vericoding
Vericoding is the method. People review the specification, and the check is against that specification rather than against a sample of tests. The same standard is how we prove concurrent code. Our experiments show the method on protocols and parsers: SpecAMQP and parsebot. They are research results, not security certifications.
Discuss the component or the workflow
Tell us the component, the workflow, and the failure you cannot afford.