Formal verification for cloud, protocols & AI

Mathematical proof of security posture — across every possible input.

Penetration tests, code audits and policy reviews sample a handful of cases and infer the rest. PrimusCredence compiles your access policies, network topology, smart contracts, distributed protocols, low-level code and AI guardrails into logic, then uses automated reasoning to settle the question exhaustively: either a proof that a violation cannot occur, or a concrete counter-example showing exactly how it can.

policy verification · sample output

$ primus verify --policy s3-finance.json --property no-external-read

  ∀ request · ¬( principal ∉ Org ∧ action = s3:GetObject
                ∧ resource = finance-data/* )

  translating policy → SMT ..................... ok
  solving over entire request space ............ ok

  SAT — counter-example found
    principal    arn:aws:iam::94xxxxxx:root
    user-agent   "InternalApp/2.1"     (matches *InternalApp*)
    source-ip    203.0.113.9           (∉ 192.0.2.0/24)

  1 violation proven reachable. evidence bundle written.

Capabilities

Six practices, one method

Each takes an artefact you already have — a policy, a topology, a contract, a protocol, a binary, a guardrail — translates it into a precise logical model, and answers a security question over the whole input space rather than a sample of it.

Cloud access-policy verification

IAM, resource and bucket policies compiled into first-order logic over strings, numbers, dates, regular expressions and IP ranges, then checked with an SMT solver against every request that could ever arrive.

Output proof of safety, or a concrete violating request

Network reachability proofs

VPCs, route tables, security groups and firewall rules modelled as constraints, so isolation questions are settled statically — without sending a single probe packet into production.

Output proof no path exists, or the exact path

API-usage conformance

Static, pre-deployment analysis of how your code calls cloud and cryptographic SDKs — catching protocol and lifecycle misuse of credential, signing and encryption objects before it ships.

Output the offending call site and trace

Low-level code verification

Bounded model checking for firmware, bootloaders, hypervisor isolation layers and node clients — proving memory safety and state-transition correctness where a defect cannot be patched after shipment.

Output bounded proof, or a failing execution trace

Formal verification of smart contracts and distributed protocols

Contracts and protocols fail in ways testing rarely reaches. A reentrancy path that opens only under one specific call ordering. A consensus protocol that survives every scenario an engineer thought to write, yet admits a Byzantine execution that forks the chain. A bridge whose guarantee holds only while a rational actor stays rational. These are not implementation bugs to be found by sampling — they are properties of the design, and they have to be settled by proof.

For smart contracts: functional correctness against a written specification; conservation-of-value, access-control and solvency invariants; arithmetic and reentrancy safety; storage-layout and upgrade-path safety across proxy patterns. Checked exhaustively over all reachable states rather than over a test suite.

For distributed protocols: safety and liveness of consensus and state-machine replication; agreement and validity under Byzantine faults, asynchrony and partition; atomicity and economic soundness of cross-chain and bridge designs. Established through machine-checked inductive invariants and model checking in TLA+, IVy and Dafny — verifying the protocol itself, not merely one implementation of it.

Track record. The Moonshot BFT consensus protocol (DSN 2024) was verified exactly this way — its safety established by model checking and published at FMBC 2024. This is not an adjacent capability; it is where the founder's research sits.

Output machine-checked invariants, or the adversarial execution that breaks them

AI guardrail verification

An agent's permitted action envelope — tool calls, system-prompt constraints, data-access boundaries — encoded as logical constraints, then checked for whether any combination of input can drive it outside that envelope. Robustness assessment follows the methodology of ISO/IEC 24029-2, the international standard for applying formal methods to neural-network robustness.

Output proof the boundary holds, or the sequence that breaks it

The evidence layer

A proof is only useful once it becomes evidence

A solver verdict is not, by itself, something a compliance function can file. Every engagement therefore delivers the same finding in three forms, written for the three people who need it.

Governance

A control-status assertion

Owned, dated, and re-run on change — the line a board or steering committee reads, with a named owner and a verification cadence.

Risk

A register entry with a delta

Likelihood moved from a qualitative estimate to either not reachable under the modelled conditions or confirmed exploitable — with the residual risk stated honestly.

Compliance

An artefact tied to a clause

Mapped to the specific control it evidences, timestamped, and reproducible — built to slot into your existing audit, not to replace it.

PrimusCredence does not issue certificates and is not an independent auditor. We produce the technical evidence your assessors, certification body and regulator rely upon — which is precisely why our work strengthens their opinion rather than competing with it.

Who we work with

Built for organisations that must prove it, not assert it

Web3 smart contracts & digital assets

Token issuers, DeFi protocols, custody platforms and virtual-asset service providers — where a single contract defect is unrecoverable once deployed, and where the regulator has begun naming the technique directly. Dubai's VARA Technology and Information Rulebook expects "independent third-party audits before deployment and formal verification where applicable" as part of its smart-contract security standard.

VARAcontract invariantsreentrancyupgrade safetysolvency

Distributed protocols & consensus

Layer-1 and Layer-2 core teams, bridge and sequencer designers, validator networks — and distributed systems well beyond Web3, including replication layers and sovereign-cloud control planes. Wherever the correctness argument depends on how nodes behave under failure, asynchrony and adversarial conditions, testing cannot reach the property and a proof can.

BFT consensussafety & livenessTLA+IVycross-chain

Cloud service providers

Tenant-isolation and access-control proofs you can hand to your own enterprise and government customers — turning an assurance question you currently answer with documentation into one you answer with evidence.

tenant isolationIAM semanticsmulti-cloud

Sovereign AI cloud

Technical assurance for AI platforms carrying national and regulated workloads, where accuracy, robustness and adversarial resilience must be demonstrated rather than asserted.

EU AI Act Art. 15ISO/IEC 42001ISO/IEC 24029-2NIST AI RMF

Banks & financial institutions

Evidence for AI model inventories, bias and robustness testing, and access-control review — under supervisory expectations that have begun to name AI governance and model risk explicitly.

CBUAEDFSAADGM FSRASAMA

Critical infrastructure & government

Network isolation proofs, firmware and control-system verification, and supplier assurance evidence for entities operating under national information-assurance mandates.

UAE IASDESC ISRNCA ECCDIFC Reg. 10

Where engagements start

The Micro-Proof Assessment

A bounded, low-cost first engagement on one slice of your environment — a policy set, a network segment, a single contract, or one protocol property. It exists so you can judge the method on your own infrastructure rather than on a slide.

You scope it narrowly — one non-production account, one network segment, one contract, or one protocol property. Read-only access is enough.
We model it and run the proofs — days, not weeks, because the toolchain is built for this rather than assembled per engagement.
You receive the counter-example — if one exists, the exact request, path, call ordering or adversarial execution that reaches the violation, reproducible on your side.
You receive the regulatory mapping — the specific control the finding bears on, so it can go straight to whoever owns that control.
You decide what happens next. No retainer is implied, and nothing obliges you to continue.

Founder

Twenty-two years of program analysis, cryptography and formal verification

Dr. Raghavendra Ramesh

Founder · PrimusCredence

PrimusCredence was founded to bring automated reasoning — the discipline behind formally verified protocols, compilers and operating systems — to cloud, protocol and AI security across MENAT.

Dr. Raghavendra holds a PhD and MSc (Engg) in Computer Science from the Indian Institute of Science, Bangalore, where he was a Microsoft PhD Fellow. His work spans program analysis, mathematical logic, automata theory, cryptography and fault-tolerant distributed systems.

At Oracle Labs he built static-analysis engines for vulnerability detection — information-flow type systems, scalable context-sensitive points-to analysis, and static detection of cursor leaks and second-order SQL injection, implemented in C++ within the Parfait/LLVM framework. At ConsenSys R&D he designed and published atomic cross-chain transaction protocols, contributing to the Atomic Crosschain Technology prototype on Hyperledger Besu. As Vice President of Research & Development at Supra he co-built a blockchain R&D division from the ground up, co-invented the Moonshot BFT consensus protocol (DSN 2024) and led its formal safety verification by model checking (FMBC 2024), co-designed the HyperNova and HyperLoop cross-chain architectures, and co-invented parallel execution and optimal sharding for deconstructed state-machine replication (VLDB 2025).

He works in Dafny, TLA+, Datalog, IVy, F#, C, C++ and Java.

Person of Indian Origin | Australian Citizen | Dubai Resident

22+Years

6US patents

16+Publications

PhDIISc Bangalore

Full publication list, patents and research whitepapers: raghavendra80.github.io