Midas Lex

Trust infrastructure for robotics.

The midas-lex CLI guides coding agents through the formal verification of Rust software using Verus, a language that builds on Rust and checks code against formal specifications. With proof annotations, Verus determines whether the code satisfies the specification. When the verifier passes, you have high confidence that the code is correct if the specification is correct.

Agents already code fast; with Verus and Midas Lex, they can code correctly.

Why Verus + Agents

Rust makes individual components safer through memory safety, strong types, and predictable performance. Midas Lex extends those guarantees across robotics infrastructure by making configurations, interfaces, assumptions, and system behavior verifiable, helping teams prevent failures before deployment.

With Midas Lex, humans express program behavior in English and focus on high-level design and declarative specifications. Agents write Verus specifications, Rust code, and proofs that the code satisfies those specifications.

Agents supply velocity. Verus supplies correctness. Midas Lex connects them.

Install

Recommended: install Rust and run:

cargo install midas-lex

Go to the latest Releases, expand Assets if it is collapsed, download the midas-lex-vx.y.z-your-platform binary (not the _private one!) and put it on your path.

The installed midas-lex is a wrapper that automatically downloads and runs the latest Midas Lex binary for your platform.

Use

Tell your agent:

Use `midas-lex` for guidance.

That's it!

Midas Lex first maps each English requirement to its public executable path, contract, abstract state transition, and verifier-checked refinement evidence. It keeps unresolved or helper-only work visible, bounds repeated proof attempts, and calls for independent semantic review before completion. Agents keep the working goal and stage record in task-owned ephemeral state, not generated files committed to your project.

Usage Details

midas-lex help

Midas Lex Helper provides end-to-end guidance for software development in Verus, from English requirements to verifier-checked public behavior.
By using midas-lex, you agree to our EULA per `midas-lex eula`.

Usage: midas-lex [COMMAND]

Commands:
  next-stage  Get guidance on what to do next given your circumstances
  docs        Get guidance for specific Verus, spec, and proof topics
  profile     Show, set, or check the Cargo.toml guidance filter (usually not needed)
  eula        Print the EULA notice
  help        Print this message or the help of the given subcommand(s)

The first run downloads the Midas Lex binary for your platform, stores the binary under MIDAS_LEX_VERUS_HOME, and then starts it. MIDAS_LEX_VERUS_HOME defaults to $XDG_DATA_HOME/midas-lex/verus when XDG_DATA_HOME is set, otherwise it defaults to $HOME/.midas-lex/verus.

Normal invocations use the latest installed ordinary Midas Lex version. After starting that binary, midas-lex may check for a newer stable release in the background. Background checks are throttled to once per hour.

Downloads and installs use one lock per data directory. The lock file is $MIDAS_LEX_VERUS_HOME/locks/install.lock.

Use a version selector to opt in to a specific release, including pre-release:

midas-lex +v0.0.1 next-stage
midas-lex +prerelease next-stage

The + selector is consumed by the wrapper, so the internal Midas Lex binary receives the remaining arguments unchanged.

To persist a selection for every project, create $MIDAS_LEX_VERUS_HOME/config.toml (or the same file under the default data directory):

version = "0.0.2-beta.1"
# Or use: prerelease = true

To select a version for one Cargo package or workspace, use its normal metadata:

[package.metadata.midas_lex]
version = "0.0.2-beta.1"
# Or use: prerelease = true

[workspace.metadata.midas_lex] is also supported and takes precedence over package metadata. Selection precedence is a command-line + selector, workspace or package metadata, the data-directory config.toml, then the ordinary default. Within project metadata, prerelease = false explicitly selects the ordinary default and suppresses a global selection. version accepts a semantic version with an optional v prefix. Do not combine version with prerelease = true. Invalid or unknown configuration values stop the wrapper with an error.

The wrapper only reads the root config.toml; runtime installs and updates write under the other data-directory paths and preserve it.

Set MIDAS_LEX_VERUS_VERBOSE=1 to show the selected runtime version tag and binary path. Set MIDAS_LEX_VERUS_LOG=info to show download and update logs.

Automatic updates

On a default invocation with a verified runtime already installed, the wrapper starts that runtime before starting one throttled background child. The child uses one stable-preferred, non-draft release lookup to check both the public wrapper and runtime for the next invocation. Network, integrity, permission, or replacement failures are warnings and do not change the current runtime command. The first run installs and starts the runtime without a background check; explicit version selectors also keep their existing direct behavior.

On Linux and macOS, a newer wrapper is verified against its exact same-name SHA-256 record, staged beside the resolved running executable, and atomically renamed over that path with its executable mode preserved. An equal or older release causes no wrapper download or notice, including when a local build is newer. On Windows, only a newer release produces a visible background warning; it names the canonical path of the running .exe and asks the user to run cargo install midas-lex --force after Midas Lex exits. Automatic runtime updates and the current command continue normally.

Releases

See docs/release.md for how wrapper releases and runtime downloads work. Release notes are committed under release-notes/.

Licenses

See LICENSES/README.md.