SysML versus Alloy

SysML Alloy
Graphical modeling language. Text modeling language.
Can export models as text XMI. Can display models graphically.
Define all the artifacts of a system, including ConOps, requirements specification, requirements traceability and verification matrices, interface definition documents (IDDs), etc. Model the parts of the system that are particularly tricky or critical. The Principle of Partiality says that Alloy models should be created for those parts of a problem that merit the cost of formalization.
The purpose of SysML is to create diagrams to communicate with your stakeholders. The purpose of Alloy is to describe a problem's concepts and relationships and then analyze them to see if there are problems with how you're thinking about the problem.
SysML parametric diagrams can be used to express constraints; constraints take the form of mathematical models. "[Parametric diagrams] is an advanced modeling practice; it requires a high degree of fidelity in your system model, something that has an associated cost." (from the book SysML Distilled, p. 179) Expressing constraints is basic in Alloy; expressing constraints is definitely not an "advanced" feature. The constraints are on sets, not mathematical equations.
Supports the object paradigm. Alloy is idiom-agnostic. It supports the object paradigm, time paradigm, event paradigm, constraint paradigm, logic paradigm, declarative paradigm, etc.
Does not support analysis and reasoning of the models created using it. Supports fully automated analysis of Alloy models. Alloy can analyze a model and identify problems in the design.
No formal underpinning. A consequence of this is that understanding of models can be more apparent than real. In some cases developers can waste considerable time resolving disputes over usage and interpretation of notations. [Evans et al] Strong formal underpinning. The foundation of Alloy is sets and set operations (join, union, intersection, difference, closure, etc.). The theory of sets has been thoroughly worked out by mathematicians, which means that Alloy has a really strong foundation.
Traditional testing process, i.e., limited testing of the model. Automated, complete testing of the model, within a bound.
Static list of definitions. No data structure that you can navigate through or operate on. The Alloy Evaluate interface allows you to enter expressions and explore the model by navigating through a model's structures (signatures and fields). The expressions can perform joins, filtering, merging, ordering, etc.
Cannot determine the equivalence of two different models. Can create two different models and then use the Alloy Analyzer to determine if the models are equivalent (i.e., if their instances are the same).
Constraints are expressed as mathematical relationships (an equation or inequality). Constraints are expressed as set relationships (join, union, intersection, closure, etc).
Can be used for mathematical modeling, but rarely used for this as there are much better tools (such as MATLAB and Simulink) for such things. Not intended for mathematical modeling, limited math support.

I understand the appeal of SysML: every component, interface, connection, and flow is digitally documented and the SysML tool keeps them all consistent. That naturally leads to to the impression that the implementation will be correct. However, that is a false impression. It is not organization that produces correctness. It is finding pesky corner cases that you hadn't considered which produces correctness. In a system with many parts, there will be lots of pesky corner cases because the human mind is unable to grapple with the complexity. To find the corner cases, you need a modeling language with a tool that can search through a vast tree, looking for the corner cases. SysML does not provide this. Alloy does.