Vehicle-lang

Latest version: v0.16.1

Safety actively analyzes 702161 Python packages for vulnerabilities to keep your Python projects secure.

Scan your dependencies

Page 1 of 4

0.16.1

* Fixed detection of Marabou timeouts.

0.16

* Decreased type-checking time by ~50%

* Decreased the size of generated verification plan files by 75%

* Improved the ordering of constraints in generated query files.

* Added better handling of verifier timeouts.

* If a verifier throws an error whilst verifying a property, Vehicle will now continue to try
verify the other properties in the file instead of immediately exiting.

* When multiple similar warnings are thrown at different indices of the same property vector (i.e. properties of type `Vector Bool n`), they are now collapsed into a single warning.

* When Vehicle has finished verifying a vector of properties, Vehicle will now output the stats about the number verified, falsified, timed-out and errored.

* Added command-line option `--no-warnings` which prevents Vehicle from printing warnings

* Added command-line option `--no-sat-print` to `vehicle verify` mode which prevents Vehicle from printing witnesses and counter-examples found during verification.

0.15

* Added functions `min` and `max` over rationals.

0.14.1

* Removed `Explicit` as a command line compilation target option as it never worked.

* Fixed bug where generated Agda files sometimes incorrectly said `Unable to read the verification cache from file`.

0.14.0

* Fixed spurious "Unnecessary resources provided" warning when exporting to ITPs.

* Drastically reduced memory consumption when compiling verification queries.

* Removed `Int` from the VCL language as not currently needed.

0.13.0

* Allow `parameter`s to be used as network sizes.

* More powerful index solver: `i` is now a valid index for vectors of size `n + 1 + i`.

* Fixed compilation bugs when using network outputs as inputs to higher order functions.

* More accurate error messages when the verifier is killed during verification.

* If during verification the verifier throws an error, Vehicle will now create a reproducer
automatically.

* Added new command-line option `--verifier-args` to `verify` mode that allows extra
arguments to be passed directly to the verifier.

* Fixed bug when reconstructing witnesses using Fourier-Motzkin elimination.

Page 1 of 4

© 2025 Safety CLI Cybersecurity Inc. All Rights Reserved.