chore: fix, Rust, lint/fmt, issues

Batch Justfile audit: standardised naming (lowercase→Justfile),
fixed parse errors, removed useless build-riscv from non-Rust repos,
added missing assail recipe, and fixed code quality issues.

Co-Authored-By: Claude Opus 4.6 (1M context) <noreply@anthropic.com>

Author: hyperpolymath

src/abi/mod.rs

@@ -115,7 +115,10 @@ pub enum TemporalProperty {
     Eventually(String),
     /// `P ~> Q` — whenever P holds, Q eventually holds.
     #[serde(rename = "leads-to")]
-    LeadsTo { antecedent: String, consequent: String },
+    LeadsTo {
+        antecedent: String,
+        consequent: String,
+    },
     /// `WF_vars(Action)` — weak fairness constraint.
     #[serde(rename = "weak-fairness")]
     WeakFairness { vars: String, action: String },
@@ -129,7 +132,10 @@ impl fmt::Display for TemporalProperty {
         match self {
             TemporalProperty::Always(p) => write!(f, "[]{}", p),
             TemporalProperty::Eventually(p) => write!(f, "<>{}", p),
-            TemporalProperty::LeadsTo { antecedent, consequent } => {
+            TemporalProperty::LeadsTo {
+                antecedent,
+                consequent,
+            } => {
                 write!(f, "{} ~> {}", antecedent, consequent)
             }
             TemporalProperty::WeakFairness { vars, action } => {
@@ -208,10 +214,7 @@ impl StateMachine {
 
         // Check: at least one state
         if self.states.is_empty() {
-            errors.push(format!(
-                "State machine '{}' has no states",
-                self.name
-            ));
+            errors.push(format!("State machine '{}' has no states", self.name));
         }
 
         // Check: no duplicate state names
@@ -356,8 +359,14 @@ mod tests {
         let sm = StateMachine {
             name: "TestMachine".to_string(),
             states: vec![
-                State { name: "Idle".into(), description: None },
-                State { name: "Running".into(), description: None },
+                State {
+                    name: "Idle".into(),
+                    description: None,
+                },
+                State {
+                    name: "Running".into(),
+                    description: None,
+                },
             ],
             initial_state: "Idle".into(),
             transitions: vec![Transition {
@@ -378,7 +387,10 @@ mod tests {
     fn test_invalid_initial_state() {
         let sm = StateMachine {
             name: "Bad".to_string(),
-            states: vec![State { name: "A".into(), description: None }],
+            states: vec![State {
+                name: "A".into(),
+                description: None,
+            }],
             initial_state: "NonExistent".into(),
             transitions: vec![],
             variables: vec![],
@@ -393,7 +405,10 @@ mod tests {
     fn test_invalid_transition_target() {
         let sm = StateMachine {
             name: "Bad".to_string(),
-            states: vec![State { name: "A".into(), description: None }],
+            states: vec![State {
+                name: "A".into(),
+                description: None,
+            }],
             initial_state: "A".into(),
             transitions: vec![Transition {
                 from: "A".into(),

src/codegen/mod.rs

@@ -81,7 +81,10 @@ pub fn generate_all(manifest: &Manifest, output_dir: &str) -> Result<()> {
 /// Currently prints the command that would be run; actual TLC invocation
 /// requires a Java runtime and the TLA+ tools jar on the PATH.
 pub fn build(manifest: &Manifest, _release: bool) -> Result<()> {
-    println!("Building tlaiser specs for project: {}", manifest.project.name);
+    println!(
+        "Building tlaiser specs for project: {}",
+        manifest.project.name
+    );
     for sm_cfg in &manifest.state_machines {
         println!(
             "  Would run TLC on {}.tla with {}.cfg",

src/codegen/parser.rs

@@ -8,7 +8,7 @@
 // TLA+-specific constraints such as identifier validity, reachability,
 // and determinism analysis.
 
-use anyhow::{bail, Result};
+use anyhow::{Result, bail};
 use std::collections::{HashMap, HashSet, VecDeque};
 
 use crate::abi::StateMachine;
@@ -25,10 +25,7 @@ use crate::abi::StateMachine;
 pub fn validate_state_machine(sm: &StateMachine) -> Result<()> {
     // Structural validation via ABI
     if let Err(errors) = sm.validate() {
-        bail!(
-            "Structural validation failed:\n  {}",
-            errors.join("\n  ")
-        );
+        bail!("Structural validation failed:\n  {}", errors.join("\n  "));
     }
 
     // Check: machine name is a valid TLA+ identifier
@@ -211,15 +208,21 @@ pub fn find_nondeterministic_states(sm: &StateMachine) -> Vec<(String, usize)> {
 #[cfg(test)]
 mod tests {
     use super::*;
-    use crate::abi::{State, Transition, StateMachine};
+    use crate::abi::{State, StateMachine, Transition};
 
     /// Helper to build a simple state machine for testing.
     fn simple_machine() -> StateMachine {
         StateMachine {
             name: "Test".to_string(),
             states: vec![
-                State { name: "A".into(), description: None },
-                State { name: "B".into(), description: None },
+                State {
+                    name: "A".into(),
+                    description: None,
+                },
+                State {
+                    name: "B".into(),
+                    description: None,
+                },
             ],
             initial_state: "A".into(),
             transitions: vec![Transition {
@@ -260,9 +263,18 @@ mod tests {
         let sm = StateMachine {
             name: "Unreachable".to_string(),
             states: vec![
-                State { name: "A".into(), description: None },
-                State { name: "B".into(), description: None },
-                State { name: "C".into(), description: None },
+                State {
+                    name: "A".into(),
+                    description: None,
+                },
+                State {
+                    name: "B".into(),
+                    description: None,
+                },
+                State {
+                    name: "C".into(),
+                    description: None,
+                },
             ],
             initial_state: "A".into(),
             transitions: vec![Transition {
@@ -286,15 +298,42 @@ mod tests {
         let sm = StateMachine {
             name: "NonDet".to_string(),
             states: vec![
-                State { name: "A".into(), description: None },
-                State { name: "B".into(), description: None },
-                State { name: "C".into(), description: None },
+                State {
+                    name: "A".into(),
+                    description: None,
+                },
+                State {
+                    name: "B".into(),
+                    description: None,
+                },
+                State {
+                    name: "C".into(),
+                    description: None,
+                },
             ],
             initial_state: "A".into(),
             transitions: vec![
-                Transition { from: "A".into(), to: "B".into(), guard: None, action: None, label: None },
-                Transition { from: "A".into(), to: "C".into(), guard: None, action: None, label: None },
-                Transition { from: "B".into(), to: "C".into(), guard: None, action: None, label: None },
+                Transition {
+                    from: "A".into(),
+                    to: "B".into(),
+                    guard: None,
+                    action: None,
+                    label: None,
+                },
+                Transition {
+                    from: "A".into(),
+                    to: "C".into(),
+                    guard: None,
+                    action: None,
+                    label: None,
+                },
+                Transition {
+                    from: "B".into(),
+                    to: "C".into(),
+                    guard: None,
+                    action: None,
+                    label: None,
+                },
             ],
             variables: vec![],
             description: None,

src/codegen/pluscal_gen.rs

@@ -29,10 +29,7 @@ pub fn generate_pluscal(sm: &StateMachine, properties: &[Property]) -> String {
 
     // Module header
     let sep = "-".repeat(4);
-    out.push_str(&format!(
-        "{} MODULE {}PlusCal {}\n",
-        sep, sm.name, sep
-    ));
+    out.push_str(&format!("{} MODULE {}PlusCal {}\n", sep, sm.name, sep));
     if let Some(ref desc) = sm.description {
         out.push_str(&format!("\\* {}\n", desc));
     }
@@ -90,10 +87,7 @@ pub fn generate_pluscal(sm: &StateMachine, properties: &[Property]) -> String {
 fn generate_algorithm_block(sm: &StateMachine) -> String {
     let mut out = String::new();
 
-    out.push_str(&format!(
-        "(* --fair algorithm {}\n",
-        sm.name
-    ));
+    out.push_str(&format!("(* --fair algorithm {}\n", sm.name));
 
     // Variables section
     out.push_str("variables\n");
@@ -128,10 +122,7 @@ fn generate_algorithm_block(sm: &StateMachine) -> String {
                 generate_single_transition(&mut out, source_state, t, sm, "            ");
             } else {
                 // Multiple transitions from same state: nested either/or
-                out.push_str(&format!(
-                    "            await state = {};\n",
-                    source_state
-                ));
+                out.push_str(&format!("            await state = {};\n", source_state));
                 let mut first_inner = true;
                 for t in transitions {
                     if first_inner {
@@ -323,9 +314,18 @@ mod tests {
         StateMachine {
             name: "MutexProtocol".to_string(),
             states: vec![
-                State { name: "Idle".into(), description: None },
-                State { name: "Waiting".into(), description: None },
-                State { name: "Critical".into(), description: None },
+                State {
+                    name: "Idle".into(),
+                    description: None,
+                },
+                State {
+                    name: "Waiting".into(),
+                    description: None,
+                },
+                State {
+                    name: "Critical".into(),
+                    description: None,
+                },
             ],
             initial_state: "Idle".into(),
             transitions: vec![

src/codegen/tla_gen.rs

@@ -87,10 +87,7 @@ fn generate_module_header(sm: &StateMachine) -> String {
     let mut header = String::new();
 
     // TLA+ module header
-    header.push_str(&format!(
-        "{} MODULE {} {}\n",
-        separator, sm.name, separator
-    ));
+    header.push_str(&format!("{} MODULE {} {}\n", separator, sm.name, separator));
 
     // Description as a comment
     if let Some(ref desc) = sm.description {
@@ -230,10 +227,7 @@ fn generate_transition_actions(sm: &StateMachine) -> String {
             if unchanged.len() == 1 {
                 section.push_str(&format!("    /\\ UNCHANGED {}\n", unchanged[0]));
             } else {
-                section.push_str(&format!(
-                    "    /\\ UNCHANGED <<{}>>\n",
-                    unchanged.join(", ")
-                ));
+                section.push_str(&format!("    /\\ UNCHANGED <<{}>>\n", unchanged.join(", ")));
             }
         }
 
@@ -425,8 +419,14 @@ mod tests {
         StateMachine {
             name: "TestSpec".to_string(),
             states: vec![
-                State { name: "Idle".into(), description: None },
-                State { name: "Running".into(), description: None },
+                State {
+                    name: "Idle".into(),
+                    description: None,
+                },
+                State {
+                    name: "Running".into(),
+                    description: None,
+                },
             ],
             initial_state: "Idle".into(),
             transitions: vec![Transition {