v1.3.1: Initial support for ViperServer, LSP and MCP servers (#307)

v1.3.1 (July 2026)

New features

• MCP and LSP servers: Nagini now ships a Model Context Protocol (MCP) server and a Language Server Protocol (LSP) server. The MCP server exposes verification to AI agents and MCP-capable editors (e.g. Claude Code, Claude Desktop, Cursor) over stdio, allowing whole files, individual methods, or inline snippets to be verified with structured diagnostics. The LSP server provides editor integration with live diagnostics and per-method verification. Install with pip install "nagini[mcp]" / pip install "nagini[lsp]".
• ViperServer backend: Verification can now run through an in-process ViperServer instance instead of invoking Silicon/Carbon directly. This enables result caching across requests, precise cancellation of running verifications, and concurrent verification of independent requests.
• Improved --server mode: The verification server now accepts and can reconfigure command-line options between requests, prints a startup message once it is ready, and the client (nagini_client) accepts a --select argument to verify only specific methods or classes on a per-request basis.
• Correctly formatted translation errors in --ide-mode: Translation errors (invalid program, unsupported feature, and type errors) are now emitted in the same file:line:col:end_line:end_col: error: message format as verification errors, so IDE/LSP frontends can parse them uniformly. Type errors now carry a real source range (start and end) rather than only a line. (#308)
• Chained comparisons: Comparison chains such as a < b < c are now supported.
• enumerate() with a start argument: enumerate(xs, start) is now supported.
• range() with a step argument: range(start, stop, step) is now supported.
• Set and dict comprehensions: Set comprehensions ({x for x in xs}) and dict comprehensions ({k: v for ... in ...}) are now supported, including comprehensions with filters and multiple generators. (#305)

Infrastructure and dependencies

• Single bundled Viper backend: The separate silicon.jar and carbon.jar backends have been replaced by a single bundled viperserver.jar, which contains Silicon, Carbon, and Silver and serves both the direct and ViperServer-based backends. Extraneous backend log output (e.g. logback traces) is now suppressed so it cannot interfere with the CLI output, the test framework, or the LSP/MCP JSON-RPC stream.
• Added optional dependency extras server, lsp, and mcp for the respective server modes.
• Added CI test workflows for the LSP/MCP servers and a test suite that runs verification through ViperServer.

---

v1.3.0 (June 2026)

New features

• Python 3.12–3.14 support: Nagini now targets Python 3.12 and newer (3.13 and 3.14 are also supported). Python versions older than 3.12 are no longer supported. (#300)
• match statement support: match/case statements are now supported in both impure and pure functions. Most pattern types (value, OR, sequence, mapping, class, wildcard, capture) are handled, with class patterns with keyword arguments currently unsupported. (#301, #302)
• Branch condition reporting: When using the Silicon backend, error messages now include the branch conditions that led to the error — the set of conditions along the execution path that the verifier was exploring when it found the failure. (#298)
• Bytearray and PByteSeq: Added support for bytearray and a corresponding pure ghost type PByteSeq. (#299)
• IntEnum support: Classes subclassing IntEnum are now supported. (#299)
• Bit shift operators: Left (<<) and right (>>) shift operators are now supported for integers. (#299)
• int.bit_length(): Added support for the int.bit_length() method. (#299)
• String format expressions: Basic support for string format operations. (#299)
• Relative imports: from .module import X style relative imports are now supported. (#280)
• Constructor calls with type arguments: Calls like ParseResult[bool](True) (generic constructor with explicit type argument) are now supported. (#264)
• Subclassing int: Soundly supports subclasses of int. Subclassing other builtin types remains unsupported. (#262)
• Better quantifier triggers for collections: Improved trigger selection for Forall quantifiers over lists, sequences, and similar collection types, reducing incompleteness issues. (#289)

Fixes

• Fixed imprecise ADT type information in certain cases. (#288)
• Fixed several crashes and translation errors. (#265, #267, #268, #272, #274, #277, #279, #283, #291)
• Fixed Reveal() annotations being incorrectly attached to type conversion wrappers rather than the actual function call. (#303)

Infrastructure and dependencies

• Migrated packaging from setup.py to pyproject.toml. (#300)
• Updated jpype1 from 1.5.0 to 1.7.0. (#300)
• Updated mypy from 0.900 to 1.5.0. (#300)
• Updated toposort from 1.5 to 1.10. (#300)
• Updated z3-solver to 4.16.0.0 on ARM. (#300)
• Updated pytest from 7.0.0 to 9.0.3. (#300)
• Removed astunparse and typed-ast dependencies. (#300)

Version 1.2.0

v1.2.0 (November 2025)

New features

• Python 3.9–3.12 multi-version support: Nagini now supports Python 3.9, 3.10, 3.11, and 3.12 (previously only 3.9 was officially supported). CI tests run against multiple Python versions. (#256)
• Opaque pure functions: Pure functions can now be marked @Opaque. Callers only learn the function's postcondition by default; they must wrap the call in Reveal(...) to unfold the function's definition. (#240)
• Assert and Unfold in pure functions: The Assert(e) and Unfold(P(...)) contract statements can now be used inside pure functions, translating to Viper's asserting and unfolding expressions. (#248)
• Postconditions with lambdas: Ensures(T, lambda r: P(r)) is now accepted as an alternative to Ensures(P(Result())). This form is fully type-checkable by mypy and executable without runtime errors. (#228)
• @Inline decorator: Methods and functions can be marked @Inline to request that Nagini inline their bodies at call sites rather than treating them modularly. (#215)
• Proper string encoding: Strings are now encoded as sequences of characters in Viper, enabling stronger reasoning about string contents. (#225)
• Optional obligation encoding: The obligation encoding (for reasoning about threads, locks, and IO operations) is now only activated when the program actually uses these features. A --force-obligations flag is available to override this. (#230)
• Using Viper's Chopper for dependency analysis: Nagini's custom dependency tracking between methods and functions has been replaced by Viper's built-in Chopper, which is more precise. (#250)
• Power operator (**): The ** operator is now supported for integers, with special-case handling for constant exponents to improve SMT automation. (#213, #217)
• Ellipsis (...): The ... literal is now accepted. (#257)
• Longer tuple support: Tuples up to length 9 are now supported (previously limited to length 4). A clear error is given for longer tuples. (#259)
• Resource bounds with Silicon: Verification is now run with resource bounds instead of timeouts by default when using the Silicon's backend. (#251)
• Viper 25.02: Updated to the Viper 25.02 release. (#226)

Fixes

• Fixed crash on dynamically indexed tuples. (#227)
• Fixed crash when calling an unsupported method or function. (#233)
• Fixed statically-bound calls to interface methods being incorrectly treated as dynamic dispatch. (#243)
• Fixed global constant functions not being marked as terminating. (#244)
• Fixed incorrect field vs. property ordering that could cause crashes. (#236)
• Fixed MayCreate and built-in predicates being usable in impure positions. (#239)

Version 1.1.1

v1.1.1 (October 2024)

Fixes

• Updated jpype1 to version 1.2.1 which has pre-built wheels for Python 3.9 on Windows and avoids compilation issues on that platform. (#210)
• Added basic Windows CI tests and fixed automatic Z3 executable path detection on Windows. (#211)

---

v1.1.0 (October 2024)

This release includes a large number of features and fixes accumulated since v0.9.0, as well as the first official support for Python 3.9.

Language and verification features

• Python 3.9 support: Nagini now supports Python 3.9 (as well as the previously supported Python 3.8). (#167)
• Abstract predicates: Predicates can now be declared abstract (without a body), allowing callers to use them without Nagini knowing their definition. (#163)
• Bitwise operators: &, |, and ^ are now supported for both booleans and bounded integers. The encoding uses the SMT bitvector theory and requires a declared bit-width bound. (#208)
• Reflected arithmetic magic methods: __radd__, __rsub__, __rmul__, etc. are now supported, enabling custom right-hand-side operator overloading. (#183)
• Unary operator magic methods: __neg__, __pos__, __abs__ etc. are now supported, also fixing a bug with negative float literals. (#184)
• Inplace arithmetic magic methods: __iadd__, __isub__, etc. are now supported. (#188)
• Float encoding options: A new --float-encoding command-line flag accepts real (model floats as mathematical reals) or ieee32 (use SMT IEEE floating point theory). The default remains uninterpreted floats. (#160)
• Float model extended: The real-number float model now handles float('inf'), float('-inf'), and float('nan'). A new isNaN() contract function is available. (#192)
• ResultT(t) contract function: ResultT(T) is a typed alternative to Result() in postconditions, allowing mypy to type-check postconditions that mention the return value without using Any. (#205)
• New dict encoding: Dictionaries are now encoded using Viper's native map type, improving completeness and counterexample quality. (#154)
• Counterexamples for generic classes: Counterexample extraction now works correctly for generic classes. (#154)
• Refute and Decreases contract functions: Added Refute(e) (assert that e is not provable) and Decreases(e) (termination measure). (#154)
• ToMS and Forall_n contract functions: Added ToMS (convert to multiset) and Forall_n (quantifier over n variables). (#154)
• viper_arg support: Arguments can be passed directly to the Viper backend via viper_arg. (#154)
• sorted() and sum() builtins: Added support for the sorted() and sum() builtin functions. (#172)
• range() with one argument: range(n) is now supported in addition to range(start, stop). (#171)
• Correct exit codes: Nagini now exits with an appropriate non-zero exit code when verification fails. (#178)
• Better error messages for built-in functions: Precondition violation messages for built-in functions include source location information via Viper annotations. (#174)
• Better tuple equality: Tuple equality is now defined in terms of component-wise object equality, and object equality is axiomatized to be transitive and symmetric. (#165, #173, #179)
• Tracking static field assignments: Static field and global variable assignments are now correctly tracked, fixing incorrect Final detection. (#162)
• Fix __truediv__: Fixed inconsistent use of __div__ vs __truediv__ (Python 3 uses the latter for /). (#190)
• Fix union subtype axiom: Fixed an unsoundness where union subtype checking was incorrect for union types on the left-hand side. (#197)
• Viper data collection: Added a --submit-for-evaluation option to submit programs to the Viper data collection server. (#180)
• Viper 24.01 update: Updated the bundled Viper backends. (#154, #166)

Version 0.9

Extensive support for information flow verification

• Verification of ordinary non-interference for sequential programs
• Verification of possibilistic and probabilistic non-interference for concurrent programs
• Counterexamples for non-interference proofs

Version 0.8.6

Major updates

• Updated dependency versions, particularly of mypy
• Compatibility with Python 3.8
• Experimental support for counterexamples

Minor changes

• Updated used Viper version to 20.07
• Improved performance for verifying top-level statements and order of declarations
• nagini_contracts is marked for mypy as containing type stubs
• Several smaller bug fixes