VERSE

Challenge

“Write-debug-test” development is pervasive across the Defense Industrial Base (DIB), even though it is well-known to be inadequate for developing high-assurance systems. Formal methods techniques and tools offer a better way forward, empowering engineers to model, analyze, and mathematically prove that a complex system behaves exactly as intended under all circumstances. This approach offers an opportunity to eliminate entire classes of vulnerabilities and errors in high-assurance, and even automatically generate correct-by-construction code based on high-level specifications.

Unfortunately, most formal methods-driven technologies suffer from limitations that prevent their widespread uptake by DIB developers. Existing techniques, languages, and tools are often both unfamiliar and difficult to learn. Formal specifications tend to be all-or-nothing (specifications without completed proofs do not provide incremental value), and are notoriously hard to maintain in the face of inevitable changes to requirements and code. 

Most importantly, previous formal approaches are typically presented as alternatives to conventional languages and development approaches, developed by and for proof experts, without serious consideration or design-time human-computer interaction (HCI) investigation of how conventional engineers could actually use them. All told, this gives developers little incentive to create specifications when coding.‍

Solution‍

With Verification Engineering for Real-world Software Engineers (VERSE), Galois is developing formal methods tools and techniques that enrich and complement existing developer practice. Our vision is that a developer can write formal specifications inline with their code, validate those specifications using low-cost testing and automated proof, and re-establish correctness quickly and intuitively when code changes. To do this, we are developing a new specification language, CN, which is designed to fit into everyday developer workflows.

Tools developed with VERSE will augment DIB developers’ existing CI and CD pipelines, allowing them to maintain continuous assurance over time as systems and specifications evolve. Developers can keep their familiar coding, development, and deployment practices while gaining immediate benefit from applying each incremental step of VERSE-enhanced proof engineering. This approach will allow DIB developers to take advantage of formal methods technologies like specification, specification-based testing, SMT-based automated proofs, interactive proof, and proof synthesis and repair, all within familiar tooling and conceptual frameworks. 

How Does It Work?

VERSE integrates formal methods directly into developers’ workflows to boost confidence in their code without disrupting familiar practices. Developers write formal specifications inline with their conventional C code, enabling verification at incremental levels—from basic assertions like data ownership to sophisticated system properties like functional correctness. These specifications can be quickly tested against implementations during development and integrated into CI/CD pipelines, ensuring continuous assurance as code evolves. 

VERSE employs tools that automate proof tasks where feasible, using SMT-based techniques, and provides intuitive semi-automated support for interactive proofs when needed. Our focus on resilience ensures that proofs adapt seamlessly to code changes, leveraging executable specifications and specification-based testing to identify and repair vulnerabilities and errors. Developers can access VERSE through standard Integrated Development Environments (IDEs) like VS Code, offering a unified, user-friendly interface that complements existing workflows while delivering both immediate and incremental benefits.

Value Add

• Empowering Formal Methods Adoption: VERSE lowers the barrier to entry for integrating formal methods, enabling developers to gradually adopt these powerful tools without disrupting existing workflows
• Immediate and Growing Value: Developers gain immediate value at every step of specification refinement, leveraging proofs and tests to progressively ensure correctness.
• Resilient Proofs for Real-World Systems: VERSE’s testing and repair mechanisms reduce maintenance overhead and give continuous assurance, making formal methods practical for evolving, high-assurance systems
• Unified Proof Engineering Environment: By embedding diverse proof technologies into familiar IDEs, VERSE offers a seamless, approachable interface for exploring and harnessing the power of formal methods‍
• Human-Centric Design: Tailored to engineers’ existing workflows and languages, VERSE incorporates continuous feedback and HCI research, ensuring tools effectively fit real-world development practices