-1600x1000.png)
Pruvendo, a company focused on mathematically proven security, has completed a formal verification of Nitrogen - Molecula Ethereum smart contract suite. Formal verification is the process of providing mathematical proof that every function behaves exactly as specified.
This costly and time-consuming procedure marks a crucial milestone in our overall security strategy, which is built around a commitment to mitigating all potential security concerns that can be addressed.
All critical and major issues were fixed before sign-off, and Pruvendo recommended the contracts for mainnet deployment.
Scope of the Verification
The review covered deposits, redemptions, yield accrual, and portfolio rebalancing inside Nitrogen. Working through a seven-stage deductive flow, Pruvendo moved from plain-language diagrams to Coq-checked* proofs by translating Solidity into Ursus* intermediate language and machine-checking each argument against the final specification.
“Note: Coq is an interactive theorem-proving language. Ursus is Pruvendo's Coq-embedded language, designed to translate Solidity code and perform formal verification of the specification.“
Important to Know
- Pruvendo report claims zero outstanding critical, high, or major issues.
- Minor informational notes that remain do not affect security or financial aspects.
- Proofs confirm code versus specification accuracy; however, they do not evaluate business logic, which has been addressed through the Halborn audit.
Next Steps
Pending formal verification of the Tron blockchain and cross-chain modules suite named Carbon, while keeping all contracts open-source for independent reviews.
Get Involved
Read the Pruvendo report, inspect the Coq proofs, or join the discussion in Molecula Discord—security is a collective effort.
