Formal Verification Services

OCamlPro provides advanced formal verification services to mathematically prove that software code correctly implements its formal specification. This service is particularly valuable for smart contracts, safety-critical embedded systems, and security-sensitive applications where bugs could have catastrophic consequences.

Verification Approach

OCamlPro employs two primary formal verification technologies:

Coq Proof Assistant: An interactive theorem prover used to construct mathematical proofs of program correctness. Coq can verify models, prove properties about programs, and even generate running code from verified specifications. The team has used Coq to achieve EAL6+ Common Criteria certification for Samsung smart card bootloaders, authentication mechanisms, and security policy models.

Why3 Platform with Alt-Ergo: A framework for deductive verification that can prove properties directly on source code. Why3 generates verification conditions from annotated programs and dispatches them to automatic theorem provers including Alt-Ergo (maintained by OCamlPro), enabling push-button verification for many properties without manual proof construction.

Smart Contract Verification

Smart contracts are ideal candidates for formal verification due to their relatively small size and simple, well-defined execution environments. OCamlPro developed a complete formalization of the EverScale Smart Contract Virtual Machine in 2021, which they use to verify Solidity smart contracts deployed on that blockchain. This formalization enables proving critical properties like:

• Fund safety (tokens cannot be created, destroyed, or stolen)
• Access control correctness (only authorized parties can perform privileged operations)
• State consistency (contract invariants are maintained across all state transitions)
• Termination guarantees (contracts cannot enter infinite loops consuming all gas)

Integration with Auditing

OCamlPro's formal verification integrates seamlessly with their smart contract auditing services. The audit process includes formal specification writing, and for critical contracts, mathematical proofs provide the highest assurance of correctness using tools like Coq and Why3 with Alt-Ergo.

Common Criteria Certification

For systems requiring the highest levels of security assurance, OCamlPro provides EAL6+ Common Criteria certification support. At this certification level, formal verification of the security policy model is mandatory. The team co-developed certification proofs with Samsung for multiple smart card systems, with proofs audited by CEA Leti cesti and certificates delivered by ANSSI (French National Agency for Security of Software Systems), one of the world's most demanding certification agencies.

Deliverables

Formal specifications in mathematical notation, machine-checked proofs of correctness using Coq or Why3, detailed verification reports explaining what properties were proven and what assumptions were made, and for Common Criteria certification, complete certification packages meeting EAL6+ requirements.

Why Choose OCamlPro

OCamlPro's team comprises more than half Ph.D. holders in computer science with deep expertise in formal methods and program verification. Their track record includes EAL6+ certifications for Samsung, formalization of blockchain virtual machines, and maintenance of Alt-Ergo, a leading automatic theorem prover used globally for software verification. This combination of academic rigor and industrial pragmatism makes them ideal partners for organizations requiring the highest levels of software assurance.