From Faster Proofs to Trusted Silicon with LUBIS EDA

LUBIS EDA is introducing FormalOS, a platform designed to make formal verification more systematic, scalable and predictable. Built on the company’s five-stage methodology, it combines structured workflows, verification playbooks, automation, reusable verification assets and sign-off evidence within customers’ existing environments. FormalOS works across formal tools, with LUBIS engineers supporting customer teams throughout verification. AI integration is optional: customers choose whether to connect a model and control its operation. The launch matters because faster RTL generation increases the need for trustworthy verification. FormalOS aims to preserve engineering expertise, improve consistency across projects and support confident decisions before designs proceed to silicon.

For a little more background LUBIS EDA has a new white paper out:

Formal Verification in the Age of AI: Methodology, Orchestration & Trust

Here is a quick summary and why it matters:

Artificial intelligence is making it easier to generate hardware designs, verification assertions, scripts, and technical reports. Yet producing these materials faster does not automatically establish that a chip will behave correctly. That distinction drives LUBIS EDA’s white paper, Formal Verification in the Age of AI: Methodology, Orchestration & Trust. Its central argument is that reliable verification requires an organized engineering system that turns technical work into defensible evidence. AI can accelerate that system, but experienced engineers remain responsible for deciding whether its results justify sign-off.

Formal verification provides mathematical evidence that specified design properties hold under defined assumptions. Its strength depends on what engineers ask it to prove and how accurately those assumptions describe the intended operating environment. A successful proof can therefore be insufficient if the property misses an important requirement or the constraints exclude a relevant behavior. The paper argues that this surrounding engineering work has become a major obstacle to scaling formal verification. Better tools help, but unclear objectives, undocumented decisions, inconsistent reviews, and dependence on individual specialists can still undermine predictability.

LUBIS proposes addressing this problem through a five-stage methodology: Discover, Plan, Prepare, Execute, and Sign Off. Discovery establishes a shared understanding of architecture, specifications, interfaces, and design intent. Planning identifies verification objectives, technical risks, responsibilities, and the evidence needed for completion. Preparation creates the verification environment and reviews assumptions and constraints. Execution develops properties, investigates failures, assesses coverage, and adjusts strategies. Sign-off evaluates the complete evidence package, including proof results, abstractions, remaining risks, and known gaps. Each stage supports decisions that others can subsequently inspect and understand.

The paper illustrates the methodology through work in the Caliptra ecosystem, particularly the Adams Bridge post-quantum cryptography accelerator. Limited implementation documentation meant engineers first had to clarify how the hardware realized its algorithms. They then divided the complex accelerator into smaller verification targets, selecting approaches suited to arithmetic and control logic. Examples from related Caliptra work show how difficult proofs prompted revised abstractions and decomposition strategies. These cases support the paper’s argument that progress often depends on understanding and restructuring the verification problem, alongside improvements in solver capability or computing resources.

To make these practices durable across projects, LUBIS presents FormalOS as an operational platform for workflows, playbooks, reusable assets, governance, automation, and accumulated engineering knowledge. Existing formal engines continue performing proofs and coverage analysis; the platform organizes the work around them. This distinction matters because a documented methodology can lose consistency during everyday execution. Embedding decisions, reviews, and lessons into shared infrastructure aims to make expertise available beyond the engineers who originally developed it, while helping teams coordinate concurrent projects and preserve knowledge as personnel change.

Within this framework, AI assists with tasks such as drafting assertions, interpreting documentation, summarizing results, and identifying potentially reusable verification assets. The paper insists that AI-generated work must satisfy the same evidence requirements as human-authored work. Engineers must check whether triggering conditions are reachable, justify assumptions, document abstraction dependencies, and identify uncovered behavior. Otherwise, apparently successful proofs may create misplaced confidence. AI’s practical value lies in reducing preparation and search effort while leaving verification strategy, interpretation, and accountability with engineers.

Bottom line: Hardware defects discovered after fabrication can demand expensive redesigns and disrupt product schedules. Verification teams therefore need evidence that supports consequential decisions, rather than an expanding collection of generated artifacts. The paper offers a useful management principle: assess AI adoption through the quality, traceability, and completeness of verification outcomes. Its commercial context also deserves attention. The broader argument is compelling: faster engineering output increases the importance of disciplined review. Organizations that preserve expert judgment, record assumptions, expose gaps, and reuse validated knowledge can make AI assistance more valuable while maintaining a clear basis for trusting their designs.

Contact LUBIS EDA

Also Read:

Assertion-First Hardware Design and Formal Verification Services

Assertion IP (AIP) for Improved Design Verification

CEO Interview: Tobias Ludwig of LUBIS EDA