AI Meets Formal Methods: Deploying HES-SO’s Verified Code Pipeline on Exoscale
François Mouraine
At HES-SO Valais-Wallis, Professor Andrei Kucharavy, Alexander Sternfeld (Research Associate) and his team at Reliable Information Lab are pioneering a transformative approach: combining LLM-driven code generation with formal verification. Using tools like Stainless for Scala (developed at EPFL), they ensure that AI-generated code isn’t just functional, it’s provably correct.
For now research are still ongoing to improve formal verification : teams are working on reinforcement learning to resolve it. For now, team is using Scala type system and compiler to ensure safety through agentic type refinement, meaning that if the code compiles, it is safe. You can only pull it off with three programming languages (Scala, Rust and Swift), that have a sufficiently strong type system and sufficient adoption for LLMs to be able to generate their code well.
What is the difference with Static Application Security Testing (SAST) tools : we’re talking about behavioral analysis of your code. It doesn’t just look for vulnerabilities, it mathematically proves that the code adheres to its functional specifications. SAST is reactive (it finds known issues), while Scala with formal verification is proactive (it ensures the code always behaves as intended, even in unexpected scenarios).
This method combines Scala’s type system with formal verification tools like Stainless to validate critical functions against explicit, human-authored specifications. Unlike purely AI-driven approaches, it ensures that code meets formal correctness criteria, essential for applications in finance, healthcare, and critical infrastructure. While verification depends on the quality of the provided specifications, this human-AI collaboration marks a significant step forward in producing secure and reliable code.
To deploy this pipeline at scale, the team turned to Exoscale. Here’s how Exoscale’s Kubernetes-native, GPU-ready, and compliance-first infrastructure powers this innovation.
The Exoscale Solution
Security & Compliance: Swiss Sovereignty
Exoscale’s Swiss datacenters are designed to meet the stringent requirements of regulated industries by integrating advanced security and compliance features at every layer. Data sovereignty is guaranteed, with all data stored and processed exclusively within Switzerland, ensuring alignment with GDPR and FINMA regulations by default.
Access control and identity management are enforced through deep integration with Kubernetes RBAC and OIDC, enabling fine-grained, least-privilege access across environments. This ensures that permissions are dynamically assigned and revoked based on roles, minimizing exposure to unauthorized actions.
For network security, Kubernetes Network Policies and Security Groups provide granular traffic segmentation, while seamless integration with IAM allows secure embedding into CI/CD pipelines. This ensures that deployments and verification runs are not only automated but also traceable, with comprehensive audit logging capturing every action for compliance and forensic purposes.
Encryption is applied end-to-end: data at rest is protected using LUKS (Linux Unified Key Setup), while all data in transit is secured with TLS 1.3, ensuring confidentiality and integrity throughout the data lifecycle.
Cost Optimization
Cost optimization is built into the architecture by leveraging Exoscale’s scalable infrastructure. SKS Autoscaling dynamically adjusts the number of TypePilot pods[1] in response to real-time demand, ensuring resources are allocated efficiently without over-provisioning. For static assets such as frontend files and logs, Exoscale’s Object Storage (SOS) provides a cost-effective solution, reducing storage expenses while maintaining high availability and durability. This approach minimizes operational costs while preserving performance and reliability.
TypePilot instances spun up in 30 seconds and a single online console click, TypePilot container went from “off”, not burning any funds”, to ready and running. This cold start speed makes it possible for LLM product team to keep their costs under control.
End-to-End Workflow
The end-to-end workflow begins with a developer submitting a request through a web IDE hosted on Exoscale SOS. The LLM API, powered by Qwen-2.5-Coder and deployed on SKS, generates baseline Scala code based on the request. This code is then reviewed and refined by developers, who assess its alignment with project requirements and best practices.
Next, TypePilot analyzes the code, identifying potential vulnerabilities and suggesting type-safe refactors to improve robustness. These suggestions are evaluated and integrated by the development team, ensuring that the changes align with the intended design and security standards.
Once the code is refined, it is committed to a version-controlled repository, triggering the CI/CD pipeline. The pipeline runs automated tests, performs static analysis, and deploys the code to a staging environment for further validation. Formal verification / (Scala type system+Compiler), executed on dedicated Compute Instances, then validates the critical logic to ensure compliance with formal specifications.
Throughout the process, monitoring tools like Prometheus track system behavior, alerting teams to any anomalies or deviations from expected performance. Finally, following a GitOps approach, the validated and verified code is promoted to production only after manual approval and review, ensuring that every change is traceable, auditable, and aligned with operational best practices.
For more information on Professor Andrei Kucharavy’s research, you can watch Professor Kucharavy’s full session on YouTube, where he breaks down the technical nuances and practical applications.
Curious to see how this workflow performs in a real-world scenario? Deploy your own AI-powered code pipeline on Exoscale’s platform and experience the benefits of secure, scalable, and verified development.
[1]: TypePilot is used to analyze and refine Scala code, ensuring type safety and suggesting improvements to make the code more robust. They are designed to be scalable, meaning the number of pods can be dynamically adjusted based on real-time demand (autoscaling).
