epfl-lara/stainless

Stainless is a formal verification framework for Scala programs that analyzes code to prove correctness properties and generate executable artifacts. It integrates with SMT solvers to verify preconditions, postconditions, and termination, while also supporting equivalence checking and the evaluation of pure functions. The system features a modular extraction pipeline that translates Scala code into intermediate representations for verification or code generation, specifically targeting the JVM and C via the GenC backend. It includes a comprehensive standard library with verified data structures and mathematical primitives to facilitate formal reasoning within Scala applications.

38 changes.

This period established the Stainless verification framework, initializing the repository structure and integrating the Inox solver backend. It focused heavily on re-architecting the core verification engine, particularly the extraction pipeline, to support modular transformations, caching, and complex language features like imperative state and object-oriented types. The work also included building out the standard library, adding JVM code generation capabilities, and implementing a Scala 3 frontend to enable comprehensive verification and testing.

23 changes.

This period focused on introducing the GenC component to translate verified Scala code into C, featuring a multi-stage IR pipeline with tail-recursion elimination and ghost code removal. Concurrently, the core extraction engine was refactored into modular, caching-aware phases to support new Scala 3 features like local classes and indexed recursive types. The work was supported by extensive benchmark suites and integration tests for both the new C backend and the updated verification logic.

13 changes.

This period focused on introducing a new Equivalence Checking component for regression verification and expanding the Stainless library with covariant collections and algebraic structures. Significant effort was also dedicated to broadening test coverage across refinement types, the Dotty frontend, and various filtering and precondition scenarios, alongside initial Snap packaging support.

Users can now use the --eval component to evaluate parameterless functions, receiving the function's body value and whether its postcondition holds. This feature provides an alternative to verification for checking function correctness and includes a new CodeGenEvaluator option for compiled evaluation, along with detailed reporting on evaluation outcomes such as body crashes, postcondition validity, and execution time.

core/src/main/scala/stainless/evaluators · high confidence

The Coq benchmark frontend now includes a new set of Stainless verification examples (ported from Leon) covering arithmetic, lists, tuples, and pre/post-conditions, providing additional test cases for the Coq code generation pipeline.

frontends/benchmarks/coq · high confidence

The Stainless proof library now includes a new \BoundedQuantifiers\ module providing recursive functions for bounded integer quantification (\intForall\, \intExists\) and their elimination rules, alongside \Internal\ helper classes (\WithRel\, \WithProof\) and \package.scala\ definitions that enable fluent relational and equational reasoning syntax (e.g., \^^\, \==\|\, \qed\) for users writing formal proofs.

frontends/library/stainless/proof · high confidence

The \frontends/algebra\ package now includes a comprehensive set of algebraic type classes and their associated verification laws, including \Semigroup\, \Monoid\, \Group\, \AbelianGroup\, \Ring\, \Eq\, \PartialOrder\, \TotalOrder\, and various semilattices. These definitions provide formal specifications for mathematical structures, complete with law annotations (e.g., associativity, commutativity, identity) to support program verification. The update also introduces concrete implementations for common types like \BigInt\ and \Nat\, as well as utility operations such as \foldMap\ for lists and formal proofs demonstrating the equivalence of \foldLeft\ and \foldRight\ operations under monoidal structures.

frontends/algebra · high confidence

The benchmark suite in \frontends/benchmarks/sat-precondition\ now includes an arithmetic language example (\ArithLangSound.scala\) demonstrating type-safe expression evaluation, alongside new test cases for unsatisfiable preconditions (\UNSATPrecond1\ through \UNSATPrecond5\) that verify the system correctly identifies contradictory requirements, complementing the existing valid precondition benchmarks.

frontends/benchmarks/sat-precondition · high confidence

The Stainless verification library now includes its own covariant implementations of List and Option, located in the \stainless.covcollection\ package. These new types provide a verified, covariant alternative to standard Scala collections, featuring methods such as \map\, \flatMap\, \filter\, \foldLeft\, \foldRight\, \take\, \drop\, \reverse\, and \contains\, along with extensive postconditions and proof specifications to ensure correctness during formal verification.

frontends/library/stainless/covcollection · high confidence

The equivalence benchmark suite in \frontends/benchmarks/equivalence\ has been expanded with several new test cases to support regression verification. New benchmarks include \addHorn\ (based on the Automating Regression Verification paper), \fizzbuzz\, \adjlist\, \arrayContent\, \arrayHeap\, \arrayIncreasing\, \binSum\ (testing normalization with return type changes), \boardgame\ (testing adjacency bonuses and city settlement validity with multiple candidate implementations), \cloudSculpting\ (testing auxiliary function matching with argument permutation), \dup\ (testing normalization of negative inputs), \factorial\, \fibonacci\, \finiteStreams\, and \foolproof\ (testing function name collision avoidance). Each benchmark consists of a Scala source file defining model and candidate functions, along with a \test\_conf.json\ specifying the expected equivalence outcomes.

frontends/benchmarks/equivalence · high confidence

The documentation build now includes the \sphinx\_rtd\_theme\ package (version 2.0.0) within the project's Sphinx theme directory. This adds the necessary Python setup module, HTML templates (layout, breadcrumbs, footer), and localized message catalogs for multiple languages (Danish, German, English, Spanish, Estonian, Persian, French, Croatian, Hungarian, Italian), ensuring the generated documentation renders with the standard Read the Docs styling and supports internationalization.

core/src/sphinx/themes · high confidence

A new command-line utility, check-files-utils, has been added to support verification integration tests. This tool processes Scala source files, runs the Stainless verification engine, and writes the resulting verification outcomes (such as validity, errors, or preconditions) into corresponding .check files. It supports configuration via command-line options for ignoring specific files and setting parallelism levels, allowing for automated comparison of verification results in test suites.

check-files-utils · high confidence

Added a suite of new verification benchmarks in the \frontends/benchmarks/verification/valid\ directory to test Stainless language capabilities, including support for anonymous classes, boolean bitwise operators (&, \|, ^), bit-vector arithmetic, real number types, and various data structures like balanced trees and maps. Also added a benchmark for encoding \Nothing\ types and moved the \Actors\ benchmark to this location (currently disabled pending Akka dependencies).

frontends/benchmarks/verification/valid · high confidence

The termination benchmark suite has been significantly expanded with new test files across several categories. New 'looping' benchmarks were added to test non-terminating programs, including lambda calculus evaluation, numeric loops, and mutual recursion patterns. New 'false-invalid' benchmarks were introduced to cover cyclic stream implementations (Fibonacci, Hamming) and consistent termination checks. New 'rejected' benchmarks test non-strict positive types and diagonalization paradoxes. New 'unchecked-invalid' benchmarks include queue implementations and additional paradox cases. New 'valid' benchmarks cover standard algorithms like Ackermann, binomial heaps, bottom-up merge sort, and constant propagation. These additions provide broader coverage for termination analysis testing.

frontends/benchmarks/termination · high confidence

Stainless now includes an experimental feature that automatically generates Scala or C test cases from counter-examples found during verification. When a verification condition fails, the system extracts the counter-example model and synthesizes a reproducible test function (e.g., \testCase1\) that triggers the failure. These tests are written to a specified output file (defaulting to \TestCases.scala\ for Scala or a \.c\ file for C via GenC), allowing users to easily reproduce and debug verification failures. This capability is exposed via the \testgen\ and \genc-testgen\ components and requires the \--batched\ mode.

core/src/main/scala/stainless/verification · high confidence

The GenC code generation pipeline is initialized with a new set of compilation phases. This includes \ArraysLengthsExtraction\ to determine fixed array sizes from invariants, \ComputeFunCtxPhase\ to track function variable contexts, and \GhostEliminationPhase\ to remove verification-only code while converting preconditions in exported functions to runtime assertions. The pipeline also introduces \GlobalStateChecker\ to enforce rules on global state usage, \StructInliningPhase\ to optimize single-member structs, and \TailRecElimPhase\ to convert tail-recursive functions into loops. Supporting infrastructure includes \ExtraOps\ for handling GenC-specific annotations (like \@cCode.export\ and \@cCode.drop\), \IR2CPhase\ for translating the intermediate representation to C, and \TrimSymbols\ to prune unused symbols from exported functions.

core/src/main/scala/stainless/genc/phases · high confidence

This change introduces the Snap packaging infrastructure for the Stainless program verifier, enabling installation via the Snap Store. It adds the \snap/snapcraft.yaml\ manifest which configures the build environment (using Java 17, SMT solvers z3 and cvc5, and Scala 3) and defines the \stainless\ application command. Additionally, it includes local wrapper scripts (\snap/local/stainless\ and \snap/local/stainless-cli\) that set up the runtime environment and launch the Stainless JARs.

snap · high confidence

Introduces the core \CodeGeneration\ and \CompilationUnit\ components that translate Stainless programs into JVM bytecode. This change adds the infrastructure for compiling functions, ADTs, and runtime types (such as collections, BigInt, and BitVector) into Java classes, enabling the execution of verified code on the JVM via the Cafebabe library.

core/src/main/scala/stainless/codegen · high confidence

Adds the \slc-lib\ Coq library, providing foundational support for verification tasks. This includes \Booleans.v\ and \PropBool.v\ for reasoning about boolean expressions and propositions (including \propInBool\ conversion and \ifthenelse\ tactics), \Sets.v\ for set operations (union, intersection, difference, subset) with associated rewriting hints, \Ints.v\ for integer comparison lemmas, and \Tactics.v\ which aggregates these into a unified \t\_base\ proof automation strategy.

slc-lib · high confidence

Introduces the sbt-stainless plugin, enabling users to integrate Stainless verification into their SBT projects. The plugin adds settings to enable/disable verification, specify extra dependencies and resolvers, and automatically fetches and includes Stainless library sources for analysis. It also includes scripted tests to verify basic verification, ghost code handling, and actor-based concurrency models.

sbt-plugin · high confidence

This change establishes the foundational repository structure for the Stainless verification framework. It introduces the Apache 2.0 license, a Contributor License Agreement (CLA), and a contributing guide. The project is configured to use the Inox solver library as a Git submodule and specifies a default configuration file (stainless.conf.default) with Z3 and cvc5 as the default solvers. Additionally, it provides a Dockerfile for containerized builds, a CI shell script for automated testing and benchmarking, and updated documentation in the README.

(repo-wide) · high confidence

Adds a new compiler frontend for Stainless that integrates with the Dotty (Scala 3) compiler via a custom plugin. This change introduces the \StainlessPlugin\ which injects a \stainless\ phase into the Dotty compilation pipeline to extract verification conditions, alongside a \GhostAccessRewriter\ phase to handle ghost code elimination. The implementation includes \Main.scala\ to bootstrap the frontend, \DottyCompiler.scala\ to manage the compiler driver and classpath, and extensive extraction logic in \ASTExtractors.scala\, \CodeExtraction.scala\, and \StainlessExtraction.scala\ to translate Dotty's typed trees into Stainless's internal representation.

frontends/dotty/src/main · high confidence

Stainless now includes a new Equivalence Checking component that verifies whether candidate functions are equivalent to specified model functions. This feature integrates into the verification pipeline, classifying functions as valid, unequivalent, unsafe, or inconclusive based on strategies like model-first or candidate-first induction. Users can configure the checker via command-line options such as \--models\ to specify reference functions, \--norm\ for normalization, and \--equivchk-output\ to write results to JSON. The component provides detailed reports distinguishing between equivalence errors and safety issues, supporting advanced features like sub-lemma matching and weight-based pruning.

core/src/main/scala/stainless/equivchk · high confidence

Adds the GenC component to Stainless, enabling the translation of verified Scala code into C. This new feature includes a C Abstract Syntax Tree (CAST), a pipeline of transformation phases (such as ghost elimination, inlining, and tail-recursion elimination), and a C printer that outputs separate header and source files. The component integrates with the existing verification pipeline, ensuring code is verified before generation, and supports features like custom includes, export annotations, and static/pure function attributes.

core/src/main/scala/stainless/genc · high confidence

The Stainless verification engine now integrates the Inox solver backend by adding a new \InoxEncoder\ component and a \SolverFactory\ for solver instantiation. The encoder translates Stainless AST nodes (such as arrays, match expressions, and postconditions) into Inox's internal representation, while the factory manages solver selection and applies the encoder as a transformation step. This change enables Stainless to offload verification conditions to the Inox solver infrastructure.

core/src/main/scala/stainless/solvers · high confidence

This change adds the \stainless.annotation\ package, providing a comprehensive set of annotations for users to control verification behavior and C code generation. The \annotations.scala\ file introduces verification directives such as \@invariant\, \@pure\, \@extern\, \@dropVCs\, and \@traceInduct\, allowing users to specify invariants, purity, and verification tactics. The \cCode.scala\ object adds specific annotations for the GenC code generator, including \@cCode.function\ for custom C implementations, \@cCode.global\ for global state management, and \@cCode.typedef\ for type mappings. Additionally, \isabelle.scala\ provides annotations for integrating with the Isabelle proof assistant. These annotations are internal (\@ignore\) and do not appear in the final compiled code, serving purely as metadata for the Stainless toolchain.

frontends/library/stainless/annotation · high confidence

The Stainless codegen runtime library has been added to the core project, providing the standard library of data types and operations required by the code generation evaluator. This includes implementations for algebraic data types (ADT), tuples, and monitors, as well as collections such as Bag, Set, Map, and BigArray. The library also introduces support for arbitrary-precision arithmetic via BigInt and Rational, bitwise operations via BitVector, and utility functions for floating-point, string, and generic value handling.

core/src/main/scala/stainless/codegen/runtime · high confidence

The Stainless verification pipeline now includes a new 'FunctionClosure' phase that extracts local (inner) functions defined within other functions. This phase hoists nested function definitions out of their enclosing scopes, capturing necessary free variables and path conditions as parameters to create closed, standalone function definitions. This enables the verification engine to reason about local functions as first-class entities with explicit dependencies, improving the handling of nested scopes and recursive local definitions.

core/src/main/scala/stainless/extraction/innerfuns · high confidence

The bin directory now includes a suite of new scripts to streamline development and distribution. For testing, external-tests.sh and bolts-tests.sh automate running the external test suites (including a new --lite mode for faster CI checks), while stainless-actors-tests.sh handles actor verification. For distribution, package-standalone.sh builds and packages standalone artifacts with Z3 and CVC5 for Linux, macOS, and Windows, and docker-release.sh automates Docker image creation and publishing. Additionally, launcher templates (launcher.tmpl.sh, launcher-noscalaz3.tmpl.sh, etc.) and the stainless-cli script provide updated ways to run Stainless, with the CLI now using scala-cli.

bin · high confidence

The Stainless verification library now includes new packages for file I/O (\FileInputStream\, \FileOutputStream\), standard input/output (\StdIn\, \StdOut\), random number generation (\Random\), and time measurement (\Timepoint\). These components provide verified abstractions for reading and writing files, handling console input and output (including unsigned integer types), and generating random values or measuring elapsed time, with specific C code generation support for the underlying operations.

frontends/library/stainless/io · high confidence

A new \stainless.equations\ package has been added to the Stainless library, providing core types and implicit conversions for equational reasoning. This includes \ProofOps\ for chaining proofs with \because\, \EqProof\ and \EqEvidence\ for establishing equality between values with optional evidence, and \RAEqEvidence\ for right-associative equational chains. The library also exposes \trivial\ and \keepEvidence\ helpers to facilitate formal verification workflows within Stainless.

frontends/library/stainless/equations · high confidence

The \stainless.math\ package now includes a comprehensive set of mathematical primitives for verification. Users can work with fixed-size bitvectors via the new \BitVectors\ object (supporting sizes from 1 to 174 bits), perform arithmetic on natural numbers using the \Nat\ type, and verify floating-point operations through the \FdLibm\ library, which provides verified implementations of \sin\, \cos\, \tan\, \asin\, and \acos\. The package also exposes standard constants like \Pi\ and \E\ and helper objects for float/double bit manipulation.

frontends/library/stainless/math · high confidence

The \stainless.lang\ package now includes a comprehensive set of library files providing verified data structures and language primitives. Users can now utilize \Bag\, \Cell\ (for mutable state), \Either\, \Map\, \MutableMap\, \Option\, \PartialFunction\ (as \\~\>\), \Quantifiers\ (with \Forall\/\Exists\ and \Bijection\/\Injection\ helpers), \Rational\, \Real\, and \Set\. The library also exposes \StaticChecks\ for \ensuring\, \require\, and \assert\, along with \Try\/\Success\/\Failure\ and various utility methods like \ghost\, \snapshot\, and \unfold\ in the package object.

frontends/library/stainless/lang · high confidence

The Stainless verification library now includes a comprehensive set of immutable collection types, including List, IArray, CMap, and ListMap, along with their associated operations and verification lemmas. Users can now verify programs using these standard data structures, which are fully specified with preconditions, postconditions, and Isabelle/HOL mappings to support automated reasoning. The library provides core list operations (such as append, reverse, take, drop, and slice), array-like access patterns via IArray, and map functionality via ListMap, all designed to be used within Stainless's verification framework.

frontends/library/stainless/collection · high confidence

The frontend now supports two distinct extraction callback modes: a batched mode (BatchedCallBack) that collects all symbols before processing, and a split mode (SplitCallBack) that processes functions incrementally. This change introduces the --extra-deps and --extra-resolvers options to fetch and unpack external Scala source dependencies via Coursier, and adds a --debug=call-graph option to export the dependency graph as a DOT file. It also adds a --keep option to prevent filtering of library symbols and improves error reporting for missing dependencies with hints for using @extern.

core/src/main/scala/stainless/frontend · high confidence

The Stainless extraction pipeline now includes a dedicated inlining phase that processes \@inline\, \@inlineOnce\, and \@specialize\ annotations. This phase introduces several new transformation stages: \FunctionSpecialization\ handles template-based specialization by generating specialized function variants; \UnfoldOpaque\ expands opaque function calls into assumptions about their inlined bodies; \CallSiteInline\ processes explicit inline calls; \ChooseInjector\ and \ChooseEncoder\ manage existential \choose\ expressions by injecting assertions and encoding them as functions; and \FunctionInlining\ performs the actual inlining of function bodies, handling preconditions, postconditions, and synthetic functions. This replaces or augments previous extraction logic with a more structured, caching-enabled pipeline for these optimizations.

core/src/main/scala/stainless/extraction/inlining · high confidence

The full-imperative validation suite now includes a comprehensive set of new benchmark examples demonstrating the verification of mutable, heap-based data structures. These additions cover fundamental structures such as Queues (with varying invariant strengths), Stacks, and Mutable Lists, alongside more complex implementations like CellArrays, MergeSort, and a Fibonacci cache. The suite also introduces benchmarks for reasoning about heap state, including first-class heap snapshots, heap projections, and aliasing safety, providing users with concrete patterns for verifying imperative code with explicit reads/modifies clauses and ghost state.

frontends/benchmarks/full-imperative/valid · high confidence

The termination extraction pipeline now supports the @induct annotation, allowing users to specify that a function should be verified using structural induction on a specific parameter (for ADTs, integers, or bitvectors). When @induct is present, the system automatically generates the corresponding decreases clause and transformation logic, ignoring any explicit decreases clauses. Additionally, the pipeline introduces support for indexed recursive types via the \indexedAt\ construct, enabling more precise reasoning about data structures with size indices.

core/src/main/scala/stainless/extraction/termination · high confidence

The Stainless extraction pipeline now supports local classes (classes defined within a method body) and inner classes. This change introduces a new \InnerClasses\ phase that lifts local class definitions to the top level, transforming them into global classes with captured outer references and method parameters as constructor arguments. The implementation includes new AST nodes (\LocalClassDef\, \LocalMethodDef\, \LocalTypeDef\, \LetClass\, \LocalThis\, \LocalClassConstructor\, \LocalClassSelector\, \LocalMethodInvocation\, \LocalClassType\) to represent these constructs during extraction, along with dependency graph analysis, ghost traverser support, and type operations to handle local class types and their relationships with global classes.

core/src/main/scala/stainless/extraction/innerclasses · high confidence

The SumAndMax.scala file, which contained Leon verification examples for list operations such as max, sum, and size, has been removed from the valid directory. This eliminates the specific property proofs and data structures defined in that file from the project's verification suite.

valid · high confidence

The OO extraction subsystem has been restructured into a modular, caching-based pipeline. This introduces dedicated phases for ADT specialization (transforming eligible classes into algebraic data types), type encoding (mapping OO types to backend sorts), and invariant initialization (generating checks for ADT constructors). The change includes new infrastructure for dependency graph computation, symbol management, and extraction caches to ensure precise and incremental processing of classes, type definitions, and functions.

core/src/main/scala/stainless/extraction/oo · high confidence

The Stainless AST in \core/src/main/scala/stainless/ast\ has been restructured from a monolithic definition into a set of modular traits (Constructors, Deconstructors, Definitions, Expressions, Graphs, Printers, SymbolOps, TreeOps, TypeOps) that extend the underlying Inox AST. This change introduces a new \Symbol\ and \SymbolIdentifier\ system for unique identification, adds support for new AST nodes like \Passes\ and \RefinementPattern\, and implements comprehensive deconstruction logic for patterns and expressions to facilitate transformations. It also integrates call and dependency graph tracking directly into the AST symbols and updates the printer to handle new syntax like \&&&\ and \passes\ blocks.

core/src/main/scala/stainless/ast · high confidence

The method extraction logic has been restructured from a monolithic implementation into a series of distinct, composable phases (DependencyGraph, FieldAccessors, GhostTraverser, Laws, MergeInvariants, MethodLifting, MutabilityAnalyzer, Sealing, SuperCalls, SuperInvariants). Each phase now operates as a standalone extraction pipeline with its own caching strategy and context, improving modularity and maintainability. This change introduces specific behaviors such as merging class invariants into single methods, handling super calls by duplicating methods, and enforcing mutability analysis through a fixpoint computation, all while preserving the existing verification semantics.

core/src/main/scala/stainless/extraction/methods · high confidence

The strictarithmetic benchmark suite now includes comprehensive test cases for strict arithmetic behavior, covering integer overflow/underflow, bit-vector narrowing, signed/unsigned conversions, and floating-point to integer casts. Valid examples demonstrate safe operations with range guards, while invalid examples verify that the frontend rejects unsafe conversions (e.g., BigInt to Int out of range) and overflow-prone operations. The suite also introduces support for the \wrapping\ block and \@wrapping\ annotation to opt-out of overflow checks, including specific tests for floating-point NaN handling and casting within wrapping contexts.

frontends/benchmarks/strictarithmetic · high confidence

A new extraction phase, TraceInductElimination, has been introduced to the Stainless pipeline. This phase processes functions to eliminate trace induction constructs, utilizing new AST flags (traceInduct, mkTest) and integrating with the existing termination extraction logic to transform function definitions before passing them to subsequent stages.

core/src/main/scala/stainless/extraction/trace · high confidence

The \frontends/benchmarks/verification/false-valid\ directory now includes several new Scala verification tests (\ChooseByExtern\, \ChooseEmpty\, \ChooseNothing\, \Countable2\, \ForestNothing2\, \MakeFalse\, and \i1506\). These benchmarks are designed to be rejected by the verifier but currently pass, highlighting specific issues such as unsoundness in the AntiAliasing transformation (issue \#1506), incorrect handling of empty types and \Nothing\ via the \choose\ operator, and edge cases involving ADT invariants and external functions. The \README\ explicitly states that this directory contains tests that should be rejected but aren't, serving as a regression suite for these known verification gaps.

frontends/benchmarks/verification/false-valid · high confidence

The Sphinx documentation build infrastructure has been relocated into the core project under \core/src/sphinx\. This change introduces a dedicated \Makefile\ for generating HTML, PDF, and other documentation formats, along with a \conf.py\ configuration file that sets the project version to 0.9.1 and applies the \sphinx\_rtd\_theme\ for the HTML output. A \.gitignore\ file is also added to exclude the \\_build\ directory from version control.

core/src/sphinx · high confidence

The extraction pipeline in the throwing module has been updated so that the ExceptionLifting phase transforms \throw new Exception\ statements into \assert(false)\ expressions. This behavioral change means that during verification, explicit exception throws are no longer treated as exceptional control flow but are instead modeled as unreachable code paths, aligning with the fix for issue \#1512.

core/src/main/scala/stainless/extraction/throwing · high confidence

The GenC code generator now uses a structured, multi-stage Intermediate Representation (IR) pipeline (NIR, CIR, LIR, RIR, SIR, TIR) to transform Scala programs into C. This change introduces several key capabilities: tail-recursion elimination that rewrites recursive functions into labeled goto loops to prevent stack overflow and avoid infinite loops; a ClassLifter that lifts class types to their hierarchy top type to properly support tagged unions; and a Normaliser that flattens block expressions to ensure execution order matches between Scala and C. The pipeline also includes a Referentiator for managing references, a StructInliner for optimizing single-field structs, and support for unsigned types and complex array allocations.

core/src/main/scala/stainless/genc/ir · high confidence

The imperative extraction phase has been restructured into a modular pipeline of new components (AntiAliasing, EffectElaboration, EffectsAnalyzer, EffectsChecker, GhostChecker, ImperativeCleanup, etc.) that explicitly track and verify side effects, mutability, and aliasing. This change introduces rigorous checks to ensure that mutable state is handled correctly, ghost code is isolated from non-ghost effects, and aliasing is prevented or explicitly managed, fundamentally changing how imperative features are translated and verified.

core/src/main/scala/stainless/extraction/imperative · high confidence

The invalid extraction benchmark suite has been significantly expanded to cover new rejection scenarios, ensuring the extraction frontend correctly rejects programs that violate Stainless' purity, aliasing, and ghost-context rules. New tests verify that aliased fresh expressions, mutable array updates with non-fresh values, and bad field inheritance are rejected. The suite also enforces stricter checks on ghost and erased annotations, preventing access to ghost symbols outside ghost contexts and validating effects on ghost parameters. Additionally, it covers type system constraints, such as rejecting unsupported Matchable types, invalid bitvector widen/narrow operations, and improper class overrides.

frontends/benchmarks/extraction/invalid · high confidence

Users can now configure Stainless options via a \stainless.conf\ (or \.stainless.conf\) file, automatically discovered in the current directory or its parents, and explicitly enabled or disabled with the new \--config-file\ option. The tool's output has been restructured around a new \Component\ and \AbstractAnalysis\ architecture, providing richer, serializable reports that include a \validFromCache\ status and an optional extended summary (\--extended-summary\) detailing solver usage, cache hits, and transformation details.

core/src/main/scala/stainless · high confidence

The extraction subsystem now uses a structured pipeline and caching system to improve performance and error reporting. A new \CheckingTransformer\ wraps transformation steps to catch \MatchError\ exceptions and throw descriptive \CheckFailedError\ messages, making it easier to diagnose lowering failures. The \ExtractionCaches\ trait introduces a dependency-aware caching mechanism using \CacheKey\ types (such as \FunctionKey\ and \SortKey\) that track symbol dependencies, allowing for precise cache invalidation when specific identifiers change. The \ExtractionPipeline\ provides a composable API for chaining transformation phases, supporting summary tracking and context passing, which replaces the previous ad-hoc extraction logic with a more robust and maintainable architecture.

core/src/main/scala/stainless/extraction · high confidence

The xlang extraction phase has been restructured into a new pipeline that includes a ConstructsUsage phase to report the usage of specific language constructs (such as \choose\, \@extern\, and \???\) in the final summary, and a PartialFunctions phase to properly handle partial function syntax. Additionally, the TreeSanitizer now enforces stricter rules, including checks for sealed traits with no children, ghost method override consistency, and setter override constraints, providing clearer error messages for malformed code.

core/src/main/scala/stainless/extraction/xlang · high confidence

This change introduces several new utility components in the extraction pipeline: a thread-safe ConcurrentCache implementation to support safer concurrent caching; a PositionChecker trait and traverser that detects and reports missing source positions for functions, expressions, and types (accessible via the --debug=positions flag); a NamedPipeline wrapper that integrates debug output for AST trees and sizes (via --debug-objects and --debug-phases) and ensures well-formedness after each phase; and SyntheticSorts, which provides cache-friendly synthetic definitions for Option (including isEmpty and get) and ControlFlow (Return/Proceed) sorts and functions when the standard library definitions are not present.

core/src/main/scala/stainless/extraction/utils · high confidence

The Stainless verification engine now includes new lattice-based simplification strategies (OL and OCBSL) alongside a foundational Core trait and Definitions. These new transformers improve how logical expressions, particularly disjunctions and arithmetic relations, are simplified and checked for contradictions during verification. Users may see changes in verification performance and the specific simplifications applied to their proofs as the system utilizes these new lattice structures for reasoning.

core/src/main/scala/stainless/transformers/lattices · high confidence

The transformer subsystem in core/src/main/scala/stainless/transformers has been restructured to improve code organization and pattern-matching handling. A new GhostTraverser trait was introduced to correctly propagate ghost context during AST traversal, ensuring that ghost flags on variables, annotations, and function invocations are respected. The core Transformer and Traverser traits were updated to explicitly handle MatchExpr and Passes nodes, as well as pattern deconstruction, allowing for more precise transformation of pattern-matching logic. Simplification capabilities were enhanced with the addition of LatticesSimplifier (wrapping OCBSL, OL, and Bland algorithms with thread-local state), SimplifierWithSolver (integrating timeout-bound solver calls for path condition reasoning), and SimplifierWithPC (handling path-condition-aware simplification of asserts, requires, and match expressions). The PartialEvaluator was refactored to include productivity checks and unfolding step limits, while TransformerWithPC was updated to correctly manage path conditions through requires, ensures, and match cases. These changes collectively provide a more robust and modular foundation for program transformations, particularly for pattern matching and purity analysis.

core/src/main/scala/stainless/transformers · high confidence

The Stainless verification engine now includes a suite of new utility components in the utils package to support advanced verification features and improved internal organization. A new CheckFilter component enables precise function filtering for verification, supporting wildcard patterns in the --functions option to target specific code paths. Cache management has been restructured with a new Caches module that introduces a --cache-dir option (defaulting to .stainless-cache/) and supports both hash-based and binary cache formats. Serialization capabilities have been significantly expanded via new StainlessSerializer and XLangSerializer classes, adding support for a wide range of AST nodes including refinement patterns, imperative constructs (blocks, while loops, mutable maps), inner classes, and various flags. Counter-example handling is improved with a new CtexRemapping utility that remaps counter-examples back to their originating functions. Additional utilities include a FileWatcher for manual file watching in watch mode, a DependenciesFinder for computing symbol dependencies, and a LibraryFilter for managing library flag propagation in class hierarchies.

core/src/main/scala/stainless/utils · high confidence

The termination checking mechanism in the core Stainless library has been completely rewritten. The previous implementation has been removed and replaced with a new architecture in \core/src/main/scala/stainless/termination\ that uses a \ProcessingPipeline\ to coordinate a series of specialized processors. These processors include \ChainProcessor\ for analyzing recursive chains, \DecreasesProcessor\ for explicit decrease measures, \LoopProcessor\ for detecting non-termination loops, \RecursionProcessor\ for simple recursive cases, and \ControlFlowAnalysis\ for handling higher-order functions and lambdas. This change fundamentally alters how the tool verifies that functions terminate, shifting from the old logic to this new modular pipeline.

core/src/main/scala/stainless/termination · high confidence

Added Dotty-specific benchmark suite for Scala 3 features; Added Stainless verification benchmark suites; Added benchmark cases for ADT failures, list operations, and refinement pattern matching; Added benchmark files for refinement type validation; Added benchmark fixtures for filtering while loops and inner functions; Added comprehensive verification test suites for ADTs, BitVectors, and Floating-Point types; Added extraction benchmarks for Scala 3 language features and semantics; Added invalid benchmark suite for imperative heap effects; Added invalid imperative benchmark suite; Added invalid refinement benchmark cases; Added invalid verification benchmarks for ADT invariants and initialization checks; Added test suite for the Dotty frontend; Added tests for the CodeGenEvaluator; Expanded imperative benchmark suite for mutable state and aliasing; Expanded refinement type validation benchmarks; GenC benchmark suite expanded with new test cases and golden-file verification; New Scala 3 integration test infrastructure for the Dotty frontend.

The Stainless compiler and library are now built against Scala 3.10.1-RC1 (nightly build from 2026-09-03). The build configuration also updates several dependencies, including circe to version 0.14.1, scala-parallel-collections to 1.0.3, and scalatest to 3.2.9, while configuring exclusion rules to prevent conflicts with upstream Scala 3 libraries in the assembled JARs.

(dependencies) · high confidence

Written by watchdog.canine.dev from the codebase's own history, inside the signed delivery this page is composed from.

• First survey — no prior run to compare against. CAI 54.

• Code Health 81
• Architecture 99
• Maturity 55
• Readiness 49
• Security 53
• Accessibility 57

• 300 commits — 244 feature/other, 56 fixes

• frontends/benchmarks — 81 commits
• core/src — 66 commits
• (root) — 59 commits
• frontends/dotty — 26 commits
• .github/workflows — 22 commits
• frontends/library — 17 commits
• docs/RELEASE_NOTES.md — 7 commits
• bin/package-standalone.sh — 5 commits
• sbt-plugin/src — 4 commits
• frontends/common — 3 commits
• bin/stainless-cli — 2 commits
• bin/launcher-noscalaz3.tmpl.bat — 1 commit
• bin/package-sbt-plugin.sh — 1 commit
• docs/AntiAliasing.md — 1 commit
• docs/README.md — 1 commit
• frontends/scalac — 1 commit
• project/build.properties — 1 commit
• snap/local — 1 commit
• snap/snapcraft.yaml — 1 commit

• fix: Add missing case for Array typeBounds, make private final, fix minor bug in RefinementLifting
• fix: Bug fix: trivial VCs had one less cell -> assertion error in Inox table render function
• fix: Clarification and fixes for tutorial (#1794)
• fix: Claude fix
• fix: ExceptionLifting phase transforms throw new Exception into assert(false) fixes #1512 (#1521)
• fix: Fix #1529 (#1531) bug in type checking arrays
• fix: Fix #1530 (#1532) allow using old in ensuring of inner functions even if variable is unchanged
• fix: Fix EffectsAnalyzer missing effects on arguments (#1491)
• fix: Fix GenC tail-recursion elimination emitting a non-terminating loop
• fix: Fix ImperativeCleanup cleaning too much (#1500)
• fix: Fix MatchError in EffectsAnalyzer (#1492)
• fix: Fix SBT plugin by changing sonatypeOssRepos (#1528)
• fix: Fix Scala version to 3.5.0 in packaging script
• fix: Fix a bug in extraction for method calls with multiple list of arguments (#1694)
• fix: Fix a too restrictive check for pure fields in classes (#1746)
• fix: Fix an extraction bug with type synonym definitions (#1595)
• fix: Fix bugs in classtag elimination found when adapting ZipLex (#1691)
• fix: Fix crashing on receiving no input files (#1666)
• fix: Fix extraction of opaque type aliases used outside their defining scope (#1770)
• fix: Fix filtering for while loops and inner functions (#1471)
• …and 280 more

Written by watchdog.canine.dev from the codebase's own history, inside the signed delivery this page is composed from.

epfl-lara/stainless was measured the same way every project in this corpus was: the same rubric, at a pinned commit, with the result published in full. Point a surveyor at a repository you know and see whether you agree with it.