GitHub tag (latest by date)

Vehicle

Vehicle is a system for embedding logical specifications into neural networks. At its heart is the Vehicle specification language, a high-level, functional language for writing mathematically-precise specifications for your networks. For example, the following simple specification says that a network's output should be monotonically increasing with respect to its third input.

Example specification

These specifications can then automatically be compiled down to loss functions to be used when training your network. After training, the same specification can be compiled down to queries for low-level neural network solvers such as Marabou which either prove that the specification holds or produce a counter-example. Such a proof is far better than simply testing, as you can prove that the specification holds for all inputs. Verified specifications can also be exported to interactive theorem provers (ITPs) such as Agda. This in turn allows for the formal verification of larger software systems that use neural networks as subcomponents. The generated ITP code is tightly linked to the actual deployed network, so changes to the network will result in errors when checking the larger proof.

Documentation

Examples

Each of the following examples comes with an explanatory README file:

ACAS Xu - The complete specification of the ACAS Xu collision avoidance system from the Reluplex paper in a single file.
Car controller - A neural network controller that is formally proven to always keep a simple model of a car on the road in the face of noisy sensor data and an unpredictable cross-wind.
MNIST robustness - A classifier for the MNIST dataset that is proven to be robust around the images in the dataset.

In addition to the above, further examples of specifications can be found in the test suite and the corresponding output of the Vehicle compiler can be found here.

Support

If you are interested in adding support for a particular format or tool then open an issue on the Issue Tracker to discuss it with us.

Neural network formats

ONNX

Dataset formats

Solver backends

Any VNNLIB 2.0 compatible solver
Marabou

Interactive Theorem Prover backends

Download files

Download the file for your platform. If you're not sure which to choose, learn more about installing packages.

Source Distributions

No source distribution files available for this release.See tutorial on generating distribution archives.

Built Distributions

If you're not sure about the file name format, learn more about wheel file names.

The dropdown lists show the available interpreters, ABIs, and platforms. Enable javascript to be able to filter the list of wheel files.

vehicle_lang-0.27.0-cp313-cp313-win_amd64.whl (13.9 MB view details)

Uploaded Aug 19, 2026 CPython 3.13Windows x86-64

vehicle_lang-0.27.0-cp313-cp313-musllinux_1_1_x86_64.whl (23.5 MB view details)

Uploaded Aug 19, 2026 CPython 3.13musllinux: musl 1.1+ x86-64

vehicle_lang-0.27.0-cp313-cp313-manylinux_2_28_x86_64.whl (22.9 MB view details)

Uploaded Aug 19, 2026 CPython 3.13manylinux: glibc 2.28+ x86-64

vehicle_lang-0.27.0-cp313-cp313-macosx_11_0_arm64.whl (18.6 MB view details)

Uploaded Aug 19, 2026 CPython 3.13macOS 11.0+ ARM64

vehicle_lang-0.27.0-cp313-cp313-macosx_10_13_x86_64.whl (19.2 MB view details)

Uploaded Aug 19, 2026 CPython 3.13macOS 10.13+ x86-64

vehicle_lang-0.27.0-cp312-cp312-win_amd64.whl (13.9 MB view details)

Uploaded Aug 19, 2026 CPython 3.12Windows x86-64

vehicle_lang-0.27.0-cp312-cp312-musllinux_1_1_x86_64.whl (23.5 MB view details)

Uploaded Aug 19, 2026 CPython 3.12musllinux: musl 1.1+ x86-64

vehicle_lang-0.27.0-cp312-cp312-manylinux_2_28_x86_64.whl (22.9 MB view details)

Uploaded Aug 19, 2026 CPython 3.12manylinux: glibc 2.28+ x86-64

vehicle_lang-0.27.0-cp312-cp312-macosx_11_0_arm64.whl (18.6 MB view details)

Uploaded Aug 19, 2026 CPython 3.12macOS 11.0+ ARM64

vehicle_lang-0.27.0-cp312-cp312-macosx_10_13_x86_64.whl (19.2 MB view details)

Uploaded Aug 19, 2026 CPython 3.12macOS 10.13+ x86-64

vehicle_lang-0.27.0-cp311-cp311-win_amd64.whl (13.9 MB view details)

Uploaded Aug 19, 2026 CPython 3.11Windows x86-64

vehicle_lang-0.27.0-cp311-cp311-musllinux_1_1_x86_64.whl (23.5 MB view details)

Uploaded Aug 19, 2026 CPython 3.11musllinux: musl 1.1+ x86-64

vehicle_lang-0.27.0-cp311-cp311-manylinux_2_28_x86_64.whl (22.9 MB view details)

Uploaded Aug 19, 2026 CPython 3.11manylinux: glibc 2.28+ x86-64

vehicle_lang-0.27.0-cp311-cp311-macosx_11_0_arm64.whl (18.6 MB view details)

Uploaded Aug 19, 2026 CPython 3.11macOS 11.0+ ARM64

vehicle_lang-0.27.0-cp311-cp311-macosx_10_10_x86_64.whl (19.2 MB view details)

Uploaded Aug 19, 2026 CPython 3.11macOS 10.10+ x86-64

vehicle_lang-0.27.0-cp310-cp310-win_amd64.whl (13.9 MB view details)

Uploaded Aug 19, 2026 CPython 3.10Windows x86-64

vehicle_lang-0.27.0-cp310-cp310-musllinux_1_1_x86_64.whl (23.5 MB view details)

Uploaded Aug 19, 2026 CPython 3.10musllinux: musl 1.1+ x86-64

vehicle_lang-0.27.0-cp310-cp310-manylinux_2_28_x86_64.whl (22.9 MB view details)

Uploaded Aug 19, 2026 CPython 3.10manylinux: glibc 2.28+ x86-64

vehicle_lang-0.27.0-cp310-cp310-macosx_11_0_arm64.whl (18.6 MB view details)

Uploaded Aug 19, 2026 CPython 3.10macOS 11.0+ ARM64

vehicle_lang-0.27.0-cp310-cp310-macosx_10_10_x86_64.whl (19.2 MB view details)

Uploaded Aug 19, 2026 CPython 3.10macOS 10.10+ x86-64

File details

Details for the file vehicle_lang-0.27.0-cp313-cp313-win_amd64.whl.

File metadata

Download URL: vehicle_lang-0.27.0-cp313-cp313-win_amd64.whl
Upload date: Aug 19, 2026
Size: 13.9 MB
Tags: CPython 3.13, Windows x86-64
Uploaded using Trusted Publishing? Yes
Uploaded via: twine/7.0.0 CPython/3.13.14

File hashes

Hashes for vehicle_lang-0.27.0-cp313-cp313-win_amd64.whl
Algorithm	Hash digest
SHA256	`f23b099696ac284fa5fa2d772f75ff4cff23c78f39d88f0f9a5a5ad67fc1d9f9`
MD5	`5af6fae7079e37f9aea0dbbaba59e30a`
BLAKE2b-256	`1c95a59b54b827c9ee5c9a4b866e0d54a9e62c82183f7339a27c22e6a31b9738`

Algorithm	Hash digest
SHA256	`252aa6d7f153b9325019e9e83cb2bdc69d006634eda6fb2f39c057bcd658cfc9`
MD5	`ba4890047d4fe1985275cfe80f960fd7`
BLAKE2b-256	`96c65f172ffa689e18d8deba60d83dda237f4fa11b6729f0f77329f995b64820`

Algorithm	Hash digest
SHA256	`6a5584cd9a44d1807e90d26fa8865afa9d7d78b2d5c43d30ca5994f628dfbd14`
MD5	`60bad2504b3a2df0d643a1d085ebc777`
BLAKE2b-256	`ebf9a5b125a315cd8259cb2406112238da49f99cf53f29f8a9880557284b3f98`

Algorithm	Hash digest
SHA256	`8d649ddde790d95ae3a1b91b3318dc8ff36ae2a9888a2229e14e2353fccb5f83`
MD5	`7cfdeb8ae55646106d90d8f728f1524f`
BLAKE2b-256	`a658caec13e1400657fae8dadcc1f6013f21930505ec8128ce757086e9a6a847`

Algorithm	Hash digest
SHA256	`9102a1dd1ee02367d06b2a4fbe7938e8d9a0fe16ca676ae9703b5d0672d37c93`
MD5	`6edad01c0f1054feb0f1eb9f5b1f805a`
BLAKE2b-256	`e10d598f2c638a4ebc6c087839d61c84cbb26af728ef270a92e2b9ce9cc041f8`

Algorithm	Hash digest
SHA256	`c7ae8cd0418a0e914105c9367c4de524bd0e93beec40209c19774abb222e492d`
MD5	`4e43f8eb9912c926ce51a7197e25d57e`
BLAKE2b-256	`9833a78b495f2cfd2494a435ad195aac4b7d2720091a0dc953e83813ab751eb1`

Algorithm	Hash digest
SHA256	`1b8e618cb15a7479e9a50cdb559731b720482b1042e54e9911d36b472f1d5f75`
MD5	`c69b8d1fe74615483b528a561dbbd126`
BLAKE2b-256	`54cf6acc7340e76ec7d38dcd4ff1ae26b38c7c915191217a17c7e7497c69b3d5`

Algorithm	Hash digest
SHA256	`a54989c227ce16166ffebebae2c87e8cbe7ce382ca5fe06b145502243fc28c83`
MD5	`8547eae672b69afdfb60a43ac8757094`
BLAKE2b-256	`339114441baa53c1fcef9344e78d6b74b6f76e9de125a275c4e75af78e1e7bb6`

Algorithm	Hash digest
SHA256	`2d809749f2452bfff69812f79047eecd15e77f2678ef0cc5aa46b703a8be81a1`
MD5	`b9c915e6a14cd226f243f8bbb3eb72a7`
BLAKE2b-256	`9bb6cc912e65c695b64b683a020fdc1ccdf4ff7264a12586236df4c0089be3b2`

Algorithm	Hash digest
SHA256	`7ecbabb126f32304158dffcfe55ea2b0ab7c641aa0431c5078abec3eda32a8fd`
MD5	`03d606be93df08a83bc3a1639ff569a2`
BLAKE2b-256	`2961b8d2aead1555abab0c8dc306e7382b716bc1cb9e844e5f54b77680cb87bb`

Algorithm	Hash digest
SHA256	`4ba3ad40b26f728df46c93efb4b8bd4679216720334481982b18d7cceedac70d`
MD5	`6a9fd5fd6714af1b202d4c5a00fd1353`
BLAKE2b-256	`25bb417b40aa4000661e0a624459a727eb3fb9865b34d00ff90cc7ab7cadeb71`

Algorithm	Hash digest
SHA256	`aaa3f4b77241ca2edec4597c323adf8f6fcf53e026a4553e28b050422241a19d`
MD5	`e77bd9fb976ba7194a38b043abafed18`
BLAKE2b-256	`9da0b8248e62034923396ec49c0c1737b3fe345331916acc3f948b7f287c9193`

Algorithm	Hash digest
SHA256	`edd86b9769353b70c6962b37f76fb65462130e26ffeec35ae553947cab80b737`
MD5	`a78624b94a6c05ab074a573fbb7b4a4a`
BLAKE2b-256	`dbc67dfac730d7dca493ae9ca897279b125dc1307e05b1443e91e6fd57354857`

Algorithm	Hash digest
SHA256	`7faa3b302b259f2536305976a7181826dc310db98d187d751ab67b00cb6003ab`
MD5	`2db7c76f4310f9ce804e499fdd6828d5`
BLAKE2b-256	`306bc5a5ea5d3029b40a1337a06679d203df5e67e57eccbdb94a278164d10483`

Algorithm	Hash digest
SHA256	`da8bc09ffe77a55eb7a53ddcc012a773ad3d9c14e3ff4ec418e294fbae212498`
MD5	`0ea6cc8317580dc26b79cd944734a4f2`
BLAKE2b-256	`ecfcd70c9d22aa810ba82a355d0abd5ca0c7b9b46fc381d608d7a64b3e80b91a`

Algorithm	Hash digest
SHA256	`3a58cc7d66e85ccd1797908cde43afe6a8ed63022c67184364ff01293595beab`
MD5	`966e8cfc6d024d88b23da0ad1fe97693`
BLAKE2b-256	`0ba3d4c4d1cb0c380098bd7beec571d42967070ec36115e7712f36cec03afb57`

Algorithm	Hash digest
SHA256	`82aea8cba78cf0579bfd177cdf4c75f6b8cf4a4085b074b327c93ec2b8040aaa`
MD5	`61ac3747d2a7c052ae14362a227368aa`
BLAKE2b-256	`0b9ebcba1d64a757c1ea4fe0f51150108b0624e4e784fbf23a908111643f7709`

Algorithm	Hash digest
SHA256	`0bcaaf5ddcbf46cd2db30023634df5051b3e21abeaefb6be061c578e32089d44`
MD5	`27e4d5837e5845979f4faa7bb36d53bd`
BLAKE2b-256	`41a98758eb06b2461e7ecce488540b11dcf696ce721d9ab395090bb394d356b4`

Algorithm	Hash digest
SHA256	`45de02ca5ca32c272b569b4a0d22734643da5b1b0543a38ffa8c0e80752dd00d`
MD5	`d8b95659e769451752c039dd8e069e26`
BLAKE2b-256	`2b6984af03621f4a30825b576d497b670fb5d35d26df386a6fc033befe4ba848`

Algorithm	Hash digest
SHA256	`638b770c07e61e087f39300b563de634d9f84afcb1ef9129802da946837bc6d2`
MD5	`4ebb725fe4fed4506ae3a6056b6967cb`
BLAKE2b-256	`1f8a6695682e0a3a3b4905b24ae117b12e4a43a782ab6b024891cecfbc5973cd`

vehicle-lang 0.27.0

Vehicle

Documentation

Examples

Support

Neural network formats

Dataset formats

Solver backends

Interactive Theorem Prover backends

Related papers

Key dates

2 maintainers

Credits

License expression

Requires

Provides Extra

Download files

Source Distributions

Built Distributions

File details

File metadata

File hashes

Provenance

File details

File metadata

File hashes

Provenance

File details

File metadata

File hashes

Provenance

File details

File metadata

File hashes

Provenance

File details

File metadata

File hashes

Provenance

File details

File metadata

File hashes

Provenance

File details

File metadata

File hashes

Provenance

File details

File metadata

File hashes

Provenance

File details

File metadata

File hashes

Provenance

File details

File metadata

File hashes

Provenance

File details

File metadata

File hashes

Provenance

File details

File metadata

File hashes

Provenance

File details

File metadata

File hashes

Provenance

File details

File metadata

File hashes

Provenance

File details

File metadata

File hashes

Provenance

File details