PyPI GitHub tag (latest by date) GitHub Workflow Status readthedocs status pre-commit.ci status

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

Dataset formats

Solver backends

Interactive Theorem Prover backends

Related papers

Key dates

PyPI data
Data sourced directly from PyPI's database.
  • Released:
Latest release

2 maintainers

PyPI data
Data sourced directly from PyPI's database.
Avatar for matthewdaggitt from gravatar.com matthewdaggitt Avatar for wenkokke from gravatar.com wenkokke

Credits

Author: Wen Kokke

License expression

MIT
View SPDX License List

Requires

Python <3.14, >=3.10

Provides Extra

test mypy pygments numpy jax dev wheel tensorflow pytorch

Report project as malware

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.

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

Uploaded CPython 3.13Windows x86-64

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

Uploaded CPython 3.13musllinux: musl 1.1+ x86-64

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

Uploaded CPython 3.13manylinux: glibc 2.28+ x86-64

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

Uploaded CPython 3.13macOS 11.0+ ARM64

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

Uploaded CPython 3.13macOS 10.13+ x86-64

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

Uploaded CPython 3.12Windows x86-64

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

Uploaded CPython 3.12musllinux: musl 1.1+ x86-64

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

Uploaded CPython 3.12manylinux: glibc 2.28+ x86-64

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

Uploaded CPython 3.12macOS 11.0+ ARM64

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

Uploaded CPython 3.12macOS 10.13+ x86-64

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

Uploaded CPython 3.11Windows x86-64

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

Uploaded CPython 3.11musllinux: musl 1.1+ x86-64

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

Uploaded CPython 3.11manylinux: glibc 2.28+ x86-64

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

Uploaded CPython 3.11macOS 11.0+ ARM64

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

Uploaded CPython 3.11macOS 10.10+ x86-64

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

Uploaded CPython 3.10Windows x86-64

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

Uploaded CPython 3.10musllinux: musl 1.1+ x86-64

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

Uploaded CPython 3.10manylinux: glibc 2.28+ x86-64

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

Uploaded CPython 3.10macOS 11.0+ ARM64

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

Uploaded CPython 3.10macOS 10.10+ x86-64

File details

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

File metadata

File hashes

Hashes for vehicle_lang-0.27.1-cp313-cp313-win_amd64.whl
Algorithm Hash digest
SHA256 f819e68d2a87536eabb37e2916202bcb1262b7bd36728b0d2bbb0276a88c86cf
MD5 649673a6805c0548ef9edab8fbfea79f
BLAKE2b-256 c263fcbcea60a180ea9ab07f8b3acbd369f5453ad40a036cd45ef88c0f0e79ac

See more details on using hashes here.

Provenance

The following attestation bundles were made for vehicle_lang-0.27.1-cp313-cp313-win_amd64.whl:

Publisher: ci.yml on vehicle-lang/vehicle

Attestations: Values shown here reflect the state when the release was signed and may no longer be current.

File details

Details for the file vehicle_lang-0.27.1-cp313-cp313-musllinux_1_1_x86_64.whl.

File metadata

File hashes

Hashes for vehicle_lang-0.27.1-cp313-cp313-musllinux_1_1_x86_64.whl
Algorithm Hash digest
SHA256 b36f3174f55e1d5ba735b068c9f95a658afa9b3e95d7634a97a07676fac7e69f
MD5 327dda2a9a3a9ae78dc787f7af110e3e
BLAKE2b-256 420eb19c900ed223aec2e975c28f1d89ba361daebafc498886f5694a4a938349

See more details on using hashes here.

Provenance

The following attestation bundles were made for vehicle_lang-0.27.1-cp313-cp313-musllinux_1_1_x86_64.whl:

Publisher: ci.yml on vehicle-lang/vehicle

Attestations: Values shown here reflect the state when the release was signed and may no longer be current.

File details

Details for the file vehicle_lang-0.27.1-cp313-cp313-manylinux_2_28_x86_64.whl.

File metadata

File hashes

Hashes for vehicle_lang-0.27.1-cp313-cp313-manylinux_2_28_x86_64.whl
Algorithm Hash digest
SHA256 b3d0da84bbb2608a52233ba53dcca404b332162e84e7a5b315ef527885f4b82f
MD5 f1d81663c453b5c11937d93a3570ba6f
BLAKE2b-256 42c1f920e6007d7fd9328119d1026897218f29cbc43e3ef4bc42de4baa5ed1a1

See more details on using hashes here.

Provenance

The following attestation bundles were made for vehicle_lang-0.27.1-cp313-cp313-manylinux_2_28_x86_64.whl:

Publisher: ci.yml on vehicle-lang/vehicle

Attestations: Values shown here reflect the state when the release was signed and may no longer be current.

File details

Details for the file vehicle_lang-0.27.1-cp313-cp313-macosx_11_0_arm64.whl.

File metadata

File hashes

Hashes for vehicle_lang-0.27.1-cp313-cp313-macosx_11_0_arm64.whl
Algorithm Hash digest
SHA256 ca9278e47b48f504732e7d42333da7975ff5e3e9a7a8b14de16194632eaa44b2
MD5 09a5e2bf994f203e7efc3d61ed243913
BLAKE2b-256 9f07d2b7e8e71ff4e6183ddeaa9cbf8633e300b06bcc3378dabe544e36ca5f69

See more details on using hashes here.

Provenance

The following attestation bundles were made for vehicle_lang-0.27.1-cp313-cp313-macosx_11_0_arm64.whl:

Publisher: ci.yml on vehicle-lang/vehicle

Attestations: Values shown here reflect the state when the release was signed and may no longer be current.

File details

Details for the file vehicle_lang-0.27.1-cp313-cp313-macosx_10_13_x86_64.whl.

File metadata

File hashes

Hashes for vehicle_lang-0.27.1-cp313-cp313-macosx_10_13_x86_64.whl
Algorithm Hash digest
SHA256 485b3e893244cea87584bd760f95a04d366d0b59b7ceb1ef7af5464ab573a079
MD5 72be38207fa18a7693303efdb7cab4c6
BLAKE2b-256 687e25033163bd9d9465e3f524a60d61168a1934f3cc0c2954535ce5eccaa7d6

See more details on using hashes here.

Provenance

The following attestation bundles were made for vehicle_lang-0.27.1-cp313-cp313-macosx_10_13_x86_64.whl:

Publisher: ci.yml on vehicle-lang/vehicle

Attestations: Values shown here reflect the state when the release was signed and may no longer be current.

File details

Details for the file vehicle_lang-0.27.1-cp312-cp312-win_amd64.whl.

File metadata

File hashes

Hashes for vehicle_lang-0.27.1-cp312-cp312-win_amd64.whl
Algorithm Hash digest
SHA256 406261b05c61a6418ad449a294e9ae66dd5750e8ab9a7b98708bb03a9cd4961f
MD5 6f05e06ac5b8eaee8a60e63a36dc7e13
BLAKE2b-256 a76e6139bdb7fb864ec3d4d5c3de569eaae6fd32b6a88ac85f85fe19f3fd0baa

See more details on using hashes here.

Provenance

The following attestation bundles were made for vehicle_lang-0.27.1-cp312-cp312-win_amd64.whl:

Publisher: ci.yml on vehicle-lang/vehicle

Attestations: Values shown here reflect the state when the release was signed and may no longer be current.

File details

Details for the file vehicle_lang-0.27.1-cp312-cp312-musllinux_1_1_x86_64.whl.

File metadata

File hashes

Hashes for vehicle_lang-0.27.1-cp312-cp312-musllinux_1_1_x86_64.whl
Algorithm Hash digest
SHA256 9377a8df44ad2c6ef6f2c059c6045730fe64ec707c3043ae18097f828c8483ba
MD5 f9b1d8f751496cf9e799d94ba22a3521
BLAKE2b-256 4f091231d91f4f63ae5ca7073a21ce4b6c3d015acc1b697cb762ae84910e89e0

See more details on using hashes here.

Provenance

The following attestation bundles were made for vehicle_lang-0.27.1-cp312-cp312-musllinux_1_1_x86_64.whl:

Publisher: ci.yml on vehicle-lang/vehicle

Attestations: Values shown here reflect the state when the release was signed and may no longer be current.

File details

Details for the file vehicle_lang-0.27.1-cp312-cp312-manylinux_2_28_x86_64.whl.

File metadata

File hashes

Hashes for vehicle_lang-0.27.1-cp312-cp312-manylinux_2_28_x86_64.whl
Algorithm Hash digest
SHA256 b0eda17803e4e938343572963f6e8889ad1600e483bc04c8f1a259d2edbdd759
MD5 d954ca542d74e2786bf3b6282e90b5e7
BLAKE2b-256 fbd3ecc427d2ac546556a027479a380a9b929529e6892662cca6c2f7ab3ffd80

See more details on using hashes here.

Provenance

The following attestation bundles were made for vehicle_lang-0.27.1-cp312-cp312-manylinux_2_28_x86_64.whl:

Publisher: ci.yml on vehicle-lang/vehicle

Attestations: Values shown here reflect the state when the release was signed and may no longer be current.

File details

Details for the file vehicle_lang-0.27.1-cp312-cp312-macosx_11_0_arm64.whl.

File metadata

File hashes

Hashes for vehicle_lang-0.27.1-cp312-cp312-macosx_11_0_arm64.whl
Algorithm Hash digest
SHA256 436b5366dbf72d277cf562f433f442d123f9f674202c06e9efe5bcad1397443c
MD5 4369f1b2783fa19694c54739c8ef7a78
BLAKE2b-256 3ecca0a092881e11acaf24c93033b207231eefef1d7b8086681948667f650172

See more details on using hashes here.

Provenance

The following attestation bundles were made for vehicle_lang-0.27.1-cp312-cp312-macosx_11_0_arm64.whl:

Publisher: ci.yml on vehicle-lang/vehicle

Attestations: Values shown here reflect the state when the release was signed and may no longer be current.

File details

Details for the file vehicle_lang-0.27.1-cp312-cp312-macosx_10_13_x86_64.whl.

File metadata

File hashes

Hashes for vehicle_lang-0.27.1-cp312-cp312-macosx_10_13_x86_64.whl
Algorithm Hash digest
SHA256 9190144b5966f254d25b6faeefd53ab2376847954047b218c977dc4018f4a2f0
MD5 67387a683820e38ff21ace8f75dbe4f4
BLAKE2b-256 f85c31c9551ef3f6aaef57cd1a48904ce2c4accc950f20525e7b936c7dfdc8e0

See more details on using hashes here.

Provenance

The following attestation bundles were made for vehicle_lang-0.27.1-cp312-cp312-macosx_10_13_x86_64.whl:

Publisher: ci.yml on vehicle-lang/vehicle

Attestations: Values shown here reflect the state when the release was signed and may no longer be current.

File details

Details for the file vehicle_lang-0.27.1-cp311-cp311-win_amd64.whl.

File metadata

File hashes

Hashes for vehicle_lang-0.27.1-cp311-cp311-win_amd64.whl
Algorithm Hash digest
SHA256 f0dd73ca77a76886dcb59cacf63634676ee60ecbf2075807b4033189105070e5
MD5 433db4af4a23bef3e6e7651beba618b6
BLAKE2b-256 c0d295d0f4727077fd936b2c966174e6ac9119ed7fd40c37cbe26627c7cfd5d3

See more details on using hashes here.

Provenance

The following attestation bundles were made for vehicle_lang-0.27.1-cp311-cp311-win_amd64.whl:

Publisher: ci.yml on vehicle-lang/vehicle

Attestations: Values shown here reflect the state when the release was signed and may no longer be current.

File details

Details for the file vehicle_lang-0.27.1-cp311-cp311-musllinux_1_1_x86_64.whl.

File metadata

File hashes

Hashes for vehicle_lang-0.27.1-cp311-cp311-musllinux_1_1_x86_64.whl
Algorithm Hash digest
SHA256 190348d3bfd94457e0fb8b4ef1a49111f45bb35142e47ff2fb42394ec7f58cb8
MD5 f33f1ef50f776d9323b069691764c87e
BLAKE2b-256 fd67799491a05cd59814325482ff412348b5f495cb540ce8fb73294e10c841e0

See more details on using hashes here.

Provenance

The following attestation bundles were made for vehicle_lang-0.27.1-cp311-cp311-musllinux_1_1_x86_64.whl:

Publisher: ci.yml on vehicle-lang/vehicle

Attestations: Values shown here reflect the state when the release was signed and may no longer be current.

File details

Details for the file vehicle_lang-0.27.1-cp311-cp311-manylinux_2_28_x86_64.whl.

File metadata

File hashes

Hashes for vehicle_lang-0.27.1-cp311-cp311-manylinux_2_28_x86_64.whl
Algorithm Hash digest
SHA256 a8b499faa743fc1c7b855fefe6d77334ffa4064f09e042bf691c8f957c0e595c
MD5 b8a6e2366cee02881e0315b6153e1bc7
BLAKE2b-256 74d68dcac7a7d3c62bd2d8243886198f3ec07e38286c3992903be21591b1b615

See more details on using hashes here.

Provenance

The following attestation bundles were made for vehicle_lang-0.27.1-cp311-cp311-manylinux_2_28_x86_64.whl:

Publisher: ci.yml on vehicle-lang/vehicle

Attestations: Values shown here reflect the state when the release was signed and may no longer be current.

File details

Details for the file vehicle_lang-0.27.1-cp311-cp311-macosx_11_0_arm64.whl.

File metadata

File hashes

Hashes for vehicle_lang-0.27.1-cp311-cp311-macosx_11_0_arm64.whl
Algorithm Hash digest
SHA256 9edc772cb83de14326602a368a77ad0246a435cbe07c299e9c413d3caf57fb5d
MD5 b8c4dc1d4974a9bfa65cb69717e4e582
BLAKE2b-256 2c6569f1bb26bde52e8fc3c1e6ab2bda3a358446c8f895d01002cb3781eabf72

See more details on using hashes here.

Provenance

The following attestation bundles were made for vehicle_lang-0.27.1-cp311-cp311-macosx_11_0_arm64.whl:

Publisher: ci.yml on vehicle-lang/vehicle

Attestations: Values shown here reflect the state when the release was signed and may no longer be current.

File details

Details for the file vehicle_lang-0.27.1-cp311-cp311-macosx_10_10_x86_64.whl.

File metadata

File hashes

Hashes for vehicle_lang-0.27.1-cp311-cp311-macosx_10_10_x86_64.whl
Algorithm Hash digest
SHA256 3cd0d681385456663015e34bfdf85b2244fd90382d27c68dc47eaac2d5fa449b
MD5 77ffb5b37eb4c09c0b516df9602c2a64
BLAKE2b-256 146a4f17a55fbaf5666908a1ea5981e934aeac3e4d633c4b9c15c349745bcaa7

See more details on using hashes here.

Provenance

The following attestation bundles were made for vehicle_lang-0.27.1-cp311-cp311-macosx_10_10_x86_64.whl:

Publisher: ci.yml on vehicle-lang/vehicle

Attestations: Values shown here reflect the state when the release was signed and may no longer be current.

File details

Details for the file vehicle_lang-0.27.1-cp310-cp310-win_amd64.whl.

File metadata

File hashes

Hashes for vehicle_lang-0.27.1-cp310-cp310-win_amd64.whl
Algorithm Hash digest
SHA256 27390b95b6353e7a60122509d52465c20992c7927241e788c824ecde448554ea
MD5 7427bc74417ec64ef31bfe78f1f9744f
BLAKE2b-256 517b0ad4815e8349d47b957a1c1a074a9149bd61fe7c276a192c7c2a1e24205e

See more details on using hashes here.

Provenance

The following attestation bundles were made for vehicle_lang-0.27.1-cp310-cp310-win_amd64.whl:

Publisher: ci.yml on vehicle-lang/vehicle

Attestations: Values shown here reflect the state when the release was signed and may no longer be current.

File details

Details for the file vehicle_lang-0.27.1-cp310-cp310-musllinux_1_1_x86_64.whl.

File metadata

File hashes

Hashes for vehicle_lang-0.27.1-cp310-cp310-musllinux_1_1_x86_64.whl
Algorithm Hash digest
SHA256 7a1165d74f22eb090273b6694a668e1db5ef12290432696095ccc8cdc0782a85
MD5 2799b6c72e26005b4e2aaaa796f3a887
BLAKE2b-256 843c0bb0586d4af52f5b2999417d66552b60ef41324877c8001515c06a8051cf

See more details on using hashes here.

Provenance

The following attestation bundles were made for vehicle_lang-0.27.1-cp310-cp310-musllinux_1_1_x86_64.whl:

Publisher: ci.yml on vehicle-lang/vehicle

Attestations: Values shown here reflect the state when the release was signed and may no longer be current.

File details

Details for the file vehicle_lang-0.27.1-cp310-cp310-manylinux_2_28_x86_64.whl.

File metadata

File hashes

Hashes for vehicle_lang-0.27.1-cp310-cp310-manylinux_2_28_x86_64.whl
Algorithm Hash digest
SHA256 ef9f4a7c171d1a5c99caa448847d51e6fc9c479535172c0cb6dd0a0a6d5f7e40
MD5 a392faa5270f4dae04acfd2f761cf0ff
BLAKE2b-256 b23dd473f2d4a79ec49535cb1554dd13d8bcd363b0dd5e879a904f3a1f83d916

See more details on using hashes here.

Provenance

The following attestation bundles were made for vehicle_lang-0.27.1-cp310-cp310-manylinux_2_28_x86_64.whl:

Publisher: ci.yml on vehicle-lang/vehicle

Attestations: Values shown here reflect the state when the release was signed and may no longer be current.

File details

Details for the file vehicle_lang-0.27.1-cp310-cp310-macosx_11_0_arm64.whl.

File metadata

File hashes

Hashes for vehicle_lang-0.27.1-cp310-cp310-macosx_11_0_arm64.whl
Algorithm Hash digest
SHA256 7f72457d34add47ba62a63720e0db26e806744f86fea23122a58b31a0ba0e06d
MD5 ff6750ee4747f37e5e547bb97edd31d1
BLAKE2b-256 58b6751ee8e308bcf9589c4ab7d39fdd579d156667602c822edd4359adb88223

See more details on using hashes here.

Provenance

The following attestation bundles were made for vehicle_lang-0.27.1-cp310-cp310-macosx_11_0_arm64.whl:

Publisher: ci.yml on vehicle-lang/vehicle

Attestations: Values shown here reflect the state when the release was signed and may no longer be current.

File details

Details for the file vehicle_lang-0.27.1-cp310-cp310-macosx_10_10_x86_64.whl.

File metadata

File hashes

Hashes for vehicle_lang-0.27.1-cp310-cp310-macosx_10_10_x86_64.whl
Algorithm Hash digest
SHA256 d6b079b7575b9d5724763442b9e62cc33a07ae4fb851e78d99a270924224a9da
MD5 3ac6853840924d22bff8fdd0952c0d46
BLAKE2b-256 3ac3863aa13bdd1f18c85cf5a165c812378bd0478af520903a162f8e9c6ae6f0

See more details on using hashes here.

Provenance

The following attestation bundles were made for vehicle_lang-0.27.1-cp310-cp310-macosx_10_10_x86_64.whl:

Publisher: ci.yml on vehicle-lang/vehicle

Attestations: Values shown here reflect the state when the release was signed and may no longer be current.

Release history Release notifications | RSS feed

This release

0.27.1 This release

20 files

0.27.0

20 files

0.26.1

20 files

0.26.0

20 files

0.25.1

20 files

0.25.0

20 files

0.24.1

20 files

0.24.0

20 files

0.23.0

20 files

0.22.0

25 files

0.21.0

20 files

0.20.0

15 files

0.19.0

20 files

0.18.0

20 files

0.17.0

21 files

0.16.1

16 files

0.15.0

16 files

0.14.1

16 files

0.13.0

30 files

0.11.1

30 files

0.10.0

30 files

0.9.0

30 files

0.8.0

30 files

0.7.0

30 files

0.6.0

30 files

0.5.1

30 files

0.4.1

30 files

0.3.3

15 files

Anthropic, PBC Visionary sponsor Bloomberg Visionary sponsor Hudson River Trading Visionary sponsor Meta Visionary sponsor NVIDIA Visionary sponsor Microsoft Sustainability sponsor Depot Continuous Integration AWS Cloud computing and Security Sponsor Datadog Monitoring Fastly CDN Google Download Analytics Sentry Error logging StatusPage Status page