Keeping the program connected to its proof
A developer using a solver needs to connect application values to mathematical terms, express the required property, and interpret the result. A proof about a separate model is useful only when that model describes the implementation. Repeating these connections by hand creates maintenance work whenever the code or specification changes.
Several systems already automate parts of this workflow. Verus places executable Rust, specifications, and proof code in one development environment. Its supported specification-to-executable translation can generate code and equivalence proofs; the documentation distinguishes this from an unverified translation. Verus translation guide
Rust bindings also allow applications to call Z3 without changing their implementation language. Bindings still require mathematical encodings and an interpretation of returned models. The practical comparison concerns how much of that semantic work the system supplies and checks.
Verification platforms already coordinate tools
SAW coordinates proof tools and tracks their results. Its Rust tutorial includes verification of a Salsa20 implementation against a Cryptol specification. Why3 records transformations, prover versions, resource limits, and results in proof sessions, with commands to replay them after changes.
F* combines programming, dependent types, SMT automation, and tactics. Its cryptographic developments have produced deployed code. These systems establish that software, mathematics, and verification can share a working environment. They differ in their languages, supported programs, translations, and trusted components.
AI-generated code and specifications
AutoVerus uses language models to generate and repair proofs for Rust code through Verus. The broader research question is how to keep a proposed implementation tied to an independently reviewed requirement throughout such a loop.
Suppose an agent changes a packet parser. Bounds checks can establish that a read stays inside a buffer. A separate specification must establish which packets are accepted and how their fields are interpreted. Proving the bounds property does not establish the acceptance policy. If the agent changes that policy to make its proof succeed, the system should expose the changed obligation.
The Axeyum direction
Axeyum develops its computational engines and proof kernel in Rust. Its bounded Rust verifier already lowers a supported source subset into solver terms and returns bounded verdicts or concrete counterexamples. It records certificate availability separately; a successful bounded decision does not imply a kernel proof of arbitrary Rust code.
The research vision is to make connections between application code, mathematical results, and evidence reusable. The system would own the translations, preserve their assumptions, and invalidate dependent results when those assumptions change. A library result could discharge a later program obligation through a checked application of that result.
A shared implementation language can simplify embedding and maintenance. It cannot by itself establish that a translation preserves meaning or that a program meets its security requirements. Axeyum’s proposed advantage needs an end-to-end demonstration: executable code, a reviewed contract, an accepted proof route, and reuse after a relevant change. That would measure the work the developer no longer has to repeat.